Open Contractors is a project dedicated to the idea that government data must not only be available to the public, it must also be accessible and understandable. It seeks to take a difficult-to-understand database of government contracts, and provide graphics, language and context to better allow journalists and non-expert level readers to see stories in this data.
Open Contractors was part of the 2015-2016 cohort of Magic Grants. Our team consists of two people, Allison McCartney and Alexandre Gonçalves.
Allison is a graduate of the Master’s program in journalism at Stanford University, and specializes in telling stories with data applications and design.
Alex is a current PhD student in the Columbia University Graduate School of Journalism. He has a background working with both software and reporting in Brazil, and designed and maintains the Open Contractors database.
Modern reporting is increasingly reliant on using data as source of evidence - numbers on a page can prove trends and anomalies, and add context to the anecdotes told by sources.
Fortunately, many government agencies release their data openly on the web, but unfortunately much of this data is presented in a frustrating and byzantine manner. With the current public-facing government databases, journalists cannot quickly find, understand and verify government contractor data for the purposes of writing a story on a daily deadline. This means that these valuable databases go underused, and important stories go untold.
The problem with bad government open data portals is well-known and documented. In 2014 the government opened 18F, an office within the General Services Administration dedicated to improving federal digital services offerings.
Groups of journalists, entrepreneurs and citizen activists have worked on services like Census Reporter, Open Elections and Citizen Audit to help laypeople make their way through difficult data that the government hasn’t provided proper portals to.
We wanted to continue in this effort to bring better data exploration tools to the public by tackling one of the largest and most difficult government databases of all: the Federal Procurement Data System (FPDS).
Unlike some other data sets, the FPDS data does currently have a portal: USAspending. USAspending allows for people to search their dataset, access an XML API and bulk download cuts of their data, but does not context or clarity for any of the information it provides, or allow easy access to downloading the data you really want. In April 2015, the site was redesigned to make it even more difficult to navigate.
We hope that this project will add to greater public understanding of how government contracting works, and allow journalists to more quickly discover stories and sources in this data.
To design the interface for Open Contractors, we started from the ground up, interviewing journalists and activists who worked with this data to figure out what questions they would like answered more easily, and what data they considered most important.
After spending time talking to practitioners at the Washington Post, the Intercept, The Project on Government Oversight (POGO), The Wall Street Journal and The BBC, we determined that the vast size of the database and the clunky means USAspending provided for downloading were some of the biggest barriers journalists faced when using this data on a deadline.
In essense, they were caught between three equally bad choices.
The graphical interface: The GUI provided by USAspending allows for fairly easy searching, but only provides a small subset of data, which is often not enough for deep analysis. When accessing the data through the search portal, you cannot open more than one contract at a time (even if you use different tabs), and downloading the contracts will only provide you with about a tenth of the 220+ columns that are in the raw dataset. Many interesting stories are found in the columns not provided.
The bulk downloader: Provides CSV files, but the files are often far too large to be easily used in a typical spreadsheet application like Excel. It casts a wide net that needs to then be worked with and sorted afterwards. Therefore, if a journalist is looking for all the contracts provided with a certain parameter for the past 15 years, and does not know or have access to tools like SQL, this can be a very difficult task.
The API: Provides data in XML format, which is difficult and unwiedly to use, even for more seasoned data folks. Learning how to use and pull data from an API, then using the XML data that results from that query is above the level of most journalists.
Early concept drawings focused on context making, graphic representations of data and sharability of information.
But we knew we wouldn’t be able to understand how we would actually represent the data without creating the actual application.
So to start prototyping the functionality of our new application, we broke off a small subset of the data and began building a Flask application. Flask is a simple Python framework that would help us quickly mimic the functionality of a more robust application framework without creating technical debt.
The work on that version of the application helped us to refine the information we wanted to show, and determine the priority of information to the viewer.
The Flask application also allowed us to work on the functionality of the site, the general visual sensibility and the graphs and charts, as the database was being built.
To work properly, Open Contractors needed to fully take apart and rebuild the federal procurement database. The data as we received it came in the bulk flat CSV format. But to make the data more usable, we needed to turn that into a relational database. That would allow us to more easily map the relationships between companies, agencies, contracts, product or service codes, and any number of parameters contained within the database.
To do this, we downloaded a subset of the data, then began to map out the individual entities contained within the data. For example, there were many columns in the dataset related to the company that received the contract, so we bundled them up to create a separate ‘contractor’ table, that could be linked to from within each contract that it had received.
This created a relationship between each contract and the company that received it, so that they were now all related to one individual entity.
However, this was not an easy process. It’s not simple to be able to say one company mentioned in one contract is the same company as one mentioned in another contract. Companies change their names over time, or they change their addresses, so it’s difficult to be sure of these connections over time.
We decided to use the DUNS numbers–names given by the Dun and Bradstreet corporation–to start our entity consolidation. A company is given a DUNS number for every individual location they have. For example, the FedEx across the street from your place of work would have a different DUNS number than the FedEx across town. Large corporations may have hundreds or thousands of locations across the country, and therefore may have just as many DUNS numbers. However the contract data provides a ‘parent DUNS’ field that can often help link many of these disparate locations.
Companies can also change DUNS numbers when they move, and we have not yet found a solution for this. We have been exploring ways to confirm the entity consistency with outside databases that do this sort of work, like Open Corporates, but haven’t yet found a way to do this without a high chance of error.
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nam at enim facilisis, dignissim erat quis, molestie nibh. Fusce quis pulvinar lectus, quis tempor ipsum. Nulla eget ligula cursus, dictum leo eu, rhoncus diam. In ut porttitor nulla. Quisque sed lectus ornare dolor vehicula ultrices eu eu turpis. Cras feugiat, sem et sagittis tincidunt, ligula dui suscipit leo, at ultrices orci nisl et urna. Mauris tempor justo a sodales maximus. Donec euismod sollicitudin tellus eu vestibulum.
Maecenas sed rhoncus neque. Cras sagittis porttitor augue eget laoreet. Nunc ex felis, convallis nec rutrum sodales, auctor at leo. Nunc convallis porttitor fringilla. Ut posuere massa quis malesuada aliquet. Sed facilisis elementum lacinia. Nulla finibus ac tellus auctor egestas.
Proin dictum, felis eget vulputate pellentesque, elit lectus bibendum nibh, eu ultrices felis nunc nec est. Morbi sed neque lectus. Donec tristique ultricies vestibulum. Nulla accumsan euismod aliquet. Quisque id tincidunt magna, et congue odio. Sed blandit, massa eu finibus mollis, tortor ipsum tincidunt eros, quis tempor turpis sem eu ex. Aliquam eget imperdiet urna, et mattis mauris. Suspendisse id blandit magna. Phasellus vel lacinia risus. Aenean tempus fermentum leo consectetur egestas. Lorem ipsum dolor sit amet, consectetur adipiscing elit. Vestibulum vulputate interdum eros sed pretium. Morbi volutpat id mauris sit amet tempor. Quisque vel lectus nec neque commodo aliquam. Morbi efficitur, risus in pulvinar pharetra, magna sem auctor sapien, eu mollis ligula justo sit amet orci.


The number of shares predicted for your article are: {{response.shares}}
Publish on this day for maximum shares: Thursday
Publish under this category for maximum shares: World


 If you create a new beautiful theme, find a bug or propose an improvement, please send me a pull request.
Fork this repo, clone your fork and configure the remotes:
# Clone your fork of the repo into the current directory
git clone https://github.com/<your-username>/color-themes-for-google-code-prettify
# Move to the newly cloned directory
cd color-themes-for-google-code-prettify
# Assign the original repo to a remote called "upstream"
git remote add upstream https://github.com/jmblog/color-themes-for-google-code-prettify
If you cloned a while ago, get the latest changes from upstream:
git checkout master
git pull upstream master
Create a new topic branch (off the latest version of master
) to contain your feature, change, or fix:
git checkout -b <topic-branch-name>
Install dependencies:
npm install
Run local server:
npm start
src/themes.json
.src/themes/<your-theme-id>.scss
src/styles/theme-previews/<your-theme-id>.scss
Please refer to existing scss files in details.


Show Panel
Show Dialog
Show Radio
Header
First Name:
Last Name:
E-mail:
State:
California
New Jersey
New York
Radio buttons:
1
2
Single checkbox:
1
Text area:
Multi checkbox:
1
2
Header
First Name:
Last Name:
E-mail:
State:
California
New Jersey
New York
Radio buttons:
1
2
Single checkbox:
1
Text area:
Multi checkbox:
1
2
Header
Hi-diddle-ee-dee...
I’m a button, and I should get focus if my preceding
is not checked.
a sailor’s life...
for me!


Library STLCsol
The simply-typed lambda calculus in Coq.
An interactive tutorial on developing programming language
metatheory. This file uses the simply-typed lambda calculus
(STLC) to demonstrate the locally nameless representation of
lambda terms and cofinite quantification in judgments.
This tutorial concentrates on "how" to formalize STLC; for more details about "why" we use this style of development see: "Engineering Formal Metatheory", Aydemir, Chargu'eraud, Pierce, Pollack, Weirich. POPL 2008.
Tutorial authors: Brian Aydemir and Stephanie Weirich, with help from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic. Adapted from code by Arthur Chargu'eraud.
Draft of 7/14/2009
This tutorial concentrates on "how" to formalize STLC; for more details about "why" we use this style of development see: "Engineering Formal Metatheory", Aydemir, Chargu'eraud, Pierce, Pollack, Weirich. POPL 2008.
Tutorial authors: Brian Aydemir and Stephanie Weirich, with help from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic. Adapted from code by Arthur Chargu'eraud.
Draft of 7/14/2009
Contents
- Syntax of STLC
- Substitution
- Free variables
- Open
- Local closure
- Properties about basic operations
- Cofinite quantification
- Tactic support
- Typing environments
- Typing relation
- Weakening
- Substitution
- Values and evaluation
- Preservation
- Progress
- Additional properties
- Renaming
- Decidability of typechecking
- Equivalence of exist fresh and cofinite
Solutions to exercises are in STLCsol.v.
First, we import a number of definitions from the Metatheory
library (see Metatheory.v). The following command makes those
definitions available in the rest of this file. This command will
only succeed if you have already run "make" in the tutorial
directory to compile the Metatheory library.
We use a locally nameless representation for the simply-typed
lambda calculus, where bound variables are represented as natural
numbers (de Bruijn indices) and free variables are represented as
atoms.
The type atom, defined in the MetatheoryAtom library, represents names. Equality on names is decidable (eq_atom_dec), and it is possible to generate an atom fresh for any given finite set of atoms (atom_fresh).
The type atom, defined in the MetatheoryAtom library, represents names. Equality on names is decidable (eq_atom_dec), and it is possible to generate an atom fresh for any given finite set of atoms (atom_fresh).
Inductive typ : Set :=
| typ_base : typ
| typ_arrow : typ -> typ -> typ.
Inductive exp : Set :=
| bvar : nat -> exp
| fvar : atom -> exp
| abs : typ -> exp -> exp
| app : exp -> exp -> exp.
Coercion bvar : nat >-> exp.
Coercion fvar : atom >-> exp.
We declare the constructors for indices and variables to be
coercions. That way, if Coq sees a nat where it expects an
exp, it will implicitly insert an application of bvar; and
similarly for atoms.
For example, we can encode the expression (\x:b. Y x) as below. Because "Y" is free variable in this term, we need to assume an atom for this name.
For example, we can encode the expression (\x:b. Y x) as below. Because "Y" is free variable in this term, we need to assume an atom for this name.
Note that because of the coercions we may write abs (app Y 0)
instead of abs (app (fvar Y) (bvar 0)).
Below is another example: the encoding of (\x:b. \y:b. (y x)).
Below is another example: the encoding of (\x:b. \y:b. (y x)).
Exercise: Uncomment and then complete the definitions of the following
lambda calculus terms using the locally nameless representation.
"two" : \s:b->b. \z:b. s (s z)
"COMB_K" : \x:b. \y:b. x
"COMB_S" : \x:b -> b -> b.\y:b -> b.\z:b. x z (y z)
"two" : \s:b->b. \z:b. s (s z)
"COMB_K" : \x:b. \y:b. x
"COMB_S" : \x:b -> b -> b.\y:b -> b.\z:b. x z (y z)
Definition two :=
abs (typ_arrow typ_base typ_base)
(abs typ_base (app 1 (app 1 0))).
Definition COMB_K :=
abs typ_base
(abs typ_base 1).
Definition COMB_S :=
abs (typ_arrow typ_base (typ_arrow typ_base typ_base))
(abs (typ_arrow typ_base typ_base)
(abs (typ_base)
(app (app 2 0) (app 1 0)))).
There are two important advantages of the locally nameless
representation:
Weighed against these advantages are two drawbacks:
- Alpha-equivalent terms have a unique representation. We're always working up to alpha-equivalence.
- Operations such as free variable substitution and free variable calculation have simple recursive definitions (and therefore are simple to reason about).
Weighed against these advantages are two drawbacks:
- The exp datatype admits terms, such as abs 3, where indices are unbound. A term is called "locally closed" when it contains no unbound indices.
- We must define *both* bound variable & free variable substitution and reason about how these operations interact with each other.
Substitution replaces a free variable with a term. The definition
below is simple for two reasons:
- Because bound variables are represented using indices, there is no need to worry about variable capture.
- We assume that the term being substituted in is locally closed. Thus, there is no need to shift indices when passing under a binder.
Fixpoint subst (z : atom) (u : exp) (e : exp)
{struct e} : exp :=
match e with
| bvar i => bvar i
| fvar x => if x == z then u else (fvar x)
| abs t e1 => abs t (subst z u e1)
| app e1 e2 => app (subst z u e1) (subst z u e2)
end.
The Fixpoint keyword defines a Coq function. As all functions
in Coq must be total. The annotation {struct e} indicates the
termination metric---all recursive calls in this definition are
made to arguments that are structurally smaller than e.
Note also that subst uses the notation x == z for decidable atom equality. This notation is defined in the Metatheory library.
We define a notation for free variable substitution that mimics standard mathematical notation.
Note also that subst uses the notation x == z for decidable atom equality. This notation is defined in the Metatheory library.
We define a notation for free variable substitution that mimics standard mathematical notation.
To demonstrate how free variable substitution works, we need to
reason about atom equality.
The decidable atom equality function returns a sum. If the two
atoms are equal, the left branch of the sum is returned, carrying
a proof of the proposition that the atoms are equal. If they are
not equal, the right branch includes a proof of the disequality.
The demo below uses three new tactics:
The demo below uses three new tactics:
- The tactic simpl reduces a Coq expression to its normal form.
- The tactic destruct (Y==Y) considers the two possible results of the equality test.
- The tactic Case marks cases in the proof script. It takes any string as its argument, and puts that string in the hypothesis list until the case is finished.
Take-home Exercise: We can use almost the same proof script as
above to state how substitution works in the variable case. Try it
on your own.
Lemma subst_eq_var: forall (x : atom) u,
[x ~> u]x = u.
Lemma subst_neq_var : forall (x y : atom) u,
y <> x -> [x ~> u]y = y.
The function fv, defined below, calculates the set of free
variables in an expression. Because we are using a locally
nameless representation, where bound variables are represented as
indices, any name we see is a free variable of a term. In
particular, this makes the abs case simple.
Fixpoint fv (e : exp) {struct e} : atoms :=
match e with
| bvar i => empty
| fvar x => singleton x
| abs t e1 => fv e1
| app e1 e2 => (fv e1) `union` (fv e2)
end.
The type atoms represents a finite set of elements of type
atom. The notation for infix union is defined in the Metatheory
library.
Lemma f_equal_demo : forall e1 e2, e1 = e2 -> fv e1 = fv e2.
Lemma fsetdec_demo : forall (x :atom) (S : atoms),
x `in` (singleton x `union` S).
Exercise subst_fresh
To show the ease of reasoning with these definitions, we will prove a
standard result from lambda calculus: if a variable does not
appear free in a term, then substituting for it has no effect.
HINTS: Prove this lemma by induction on e.
HINTS: Prove this lemma by induction on e.
- You will need to use simpl in many cases. You can simpl everything everywhere (including hypotheses) with the pattern simpl in *.
- Part of this proof includes a false assumption about free variables. Destructing this hypothesis produces a goal about finite set membership that is solvable by fsetdec.
Lemma subst_fresh : forall (x : atom) e u,
x `notin` fv e -> [x ~> u] e = e.
Lemma subst_notin_fv : forall x y u e,
x `notin` fv e -> x `notin` fv u ->
x `notin` fv ([y ~> u]e).
Opening replaces an index with a term. It corresponds to informal
substitution for a bound variable, such as in the rule for beta
reduction. Note that only "dangling" indices (those that do not
refer to any abstraction) can be opened. Opening has no effect
for terms that are locally closed.
Natural numbers are just an inductive datatype with two constructors: O (as in the letter 'oh', not 'zero') and S, defined in Coq.Init.Datatypes. Coq allows literal natural numbers to be written using standard decimal notation, e.g., 0, 1, 2, etc. The notation k == i is the decidable equality function for natural numbers (cf. Coq.Peano_dec.eq_nat_dec). This notation is defined in the Metatheory library.
We make several simplifying assumptions in defining open_rec.
First, we assume that the argument u is locally closed. This assumption simplifies the implementation since we do not need to shift indices in u when passing under a binder. Second, we assume that this function is initially called with index zero and that zero is the only unbound index in the term. This eliminates the need to possibly subtract one in the case of indices.
There is no need to worry about variable capture because bound variables are indices.
Natural numbers are just an inductive datatype with two constructors: O (as in the letter 'oh', not 'zero') and S, defined in Coq.Init.Datatypes. Coq allows literal natural numbers to be written using standard decimal notation, e.g., 0, 1, 2, etc. The notation k == i is the decidable equality function for natural numbers (cf. Coq.Peano_dec.eq_nat_dec). This notation is defined in the Metatheory library.
We make several simplifying assumptions in defining open_rec.
First, we assume that the argument u is locally closed. This assumption simplifies the implementation since we do not need to shift indices in u when passing under a binder. Second, we assume that this function is initially called with index zero and that zero is the only unbound index in the term. This eliminates the need to possibly subtract one in the case of indices.
There is no need to worry about variable capture because bound variables are indices.
Fixpoint open_rec (k : nat) (u : exp)(e : exp)
{struct e} : exp :=
match e with
| bvar i => if k == i then u else (bvar i)
| fvar x => fvar x
| abs t e1 => abs t (open_rec (S k) u e1)
| app e1 e2 => app (open_rec k u e1) (open_rec k u e2)
end.
Many common applications of opening replace index zero with an
expression or variable. The following definition provides a
convenient shorthand for such uses. Note that the order of
arguments is switched relative to the definition above. For
example, (open e x) can be read as "substitute the variable x
for index 0 in e" and "open e with the variable x."
Recall that the coercions above let us write x in place of
(fvar x).
This next demo shows the operation of open. For example, the
locally nameless representation of the term (\y. (\x. (y x)) y) is
abs (app (abs (app 1 0)) 0). To look at the body without the
outer abstraction, we need to replace the indices that refer to
that abstraction with a name. Therefore, we show that we can open
the body of the abs above with Y to produce app (abs (app Y 0))
Y).
Recall that exp admits terms that contain unbound indices. We
say that a term is locally closed when no indices appearing in it
are unbound. The proposition lc e holds when an expression e
is locally closed.
The inductive definition below formalizes local closure such that the resulting induction principle serves as the structural induction principle over (locally closed) expressions. In particular, unlike induction for type exp, there are no cases for bound variables. Thus, the induction principle corresponds more closely to informal practice than the one arising from the definition of pre-terms.
The inductive definition below formalizes local closure such that the resulting induction principle serves as the structural induction principle over (locally closed) expressions. In particular, unlike induction for type exp, there are no cases for bound variables. Thus, the induction principle corresponds more closely to informal practice than the one arising from the definition of pre-terms.
Inductive lc : exp -> Prop :=
| lc_var : forall (x:atom),
lc x
| lc_abs : forall (x : atom) e t,
x `notin` fv e -> lc (open e x) ->
lc (abs t e)
| lc_app : forall e1 e2,
lc e1 -> lc e2 ->
lc (app e1 e2).
Hint Constructors lc.
Properties about basic operations
We also define a notation for open_rec to make stating some of
the properties simpler. However, we don't need to use open_rec
outside of this part of the tutorial so we make it a local
notation, confined to this section.
The first property we would like to show is the analogue to
subst_fresh: index substitution has no effect for closed terms.
Here is an initial attempt at the proof.
Here is an initial attempt at the proof.
At this point there are two problems. Our goal is about
substitution for index S k in term e, while our induction
hypothesis IHLC only tells use about index k in term open e x.
To solve the first problem, we generalize our IH over all k. That way, when k is incremented in the abs case, it will still apply. Below, we use the tactic generalize dependent to generalize over k before using induction.
To solve the first problem, we generalize our IH over all k. That way, when k is incremented in the abs case, it will still apply. Below, we use the tactic generalize dependent to generalize over k before using induction.
At this point we are still stuck because the IH concerns
open e x instead of e. The result that we need is that if an
index substitution has no effect for an opened term, then it has
no effect for the raw term (as long as we are *not* substituting
for 0, hence S k below).
In other words, expanding the definition of open:
Of course, to prove this result, we must generalize 0 and S k to be any pair of inequal numbers to get a strong enough induction hypothesis for the abs case.
open e x = {S k ~> u}(open e x) -> e = {S k ~> u} e
In other words, expanding the definition of open:
{0 ~> x}e = {S k ~> u}({0 ~> x} e) -> e = {S k ~> u} e
Of course, to prove this result, we must generalize 0 and S k to be any pair of inequal numbers to get a strong enough induction hypothesis for the abs case.
Lemma open_rec_lc_core : forall e j v i u,
i <> j ->
{j ~> v} e = {i ~> u} ({j ~> v} e) ->
e = {i ~> u} e.
Lemma open_rec_lc_core_automated : forall e j v i u,
i <> j ->
{j ~> v} e = {i ~> u} ({j ~> v} e) ->
e = {i ~> u} e.
With the help of this lemma, we can complete the proof.
Take-home Exercise subst_open_rec
The next lemma demonstrates that free variable substitution
distributes over index substitution.
The proof of this lemma is by straightforward induction over e1. When e1 is a free variable, we need to appeal to open_rec_lc, proved above.
The proof of this lemma is by straightforward induction over e1. When e1 is a free variable, we need to appeal to open_rec_lc, proved above.
Lemma subst_open_rec : forall e1 e2 u (x : atom) k,
lc u ->
[x ~> u] ({k ~> e2} e1) = {k ~> [x ~> u] e2} ([x ~> u] e1).
The lemma above is most often used with k = 0 and
e2 as some fresh variable. Therefore, it simplifies matters
to define the following useful corollary.
HINT: Do not use induction. Rewrite with subst_open_rec and subst_neq_var.
HINT: Do not use induction. Rewrite with subst_open_rec and subst_neq_var.
Lemma subst_open_var : forall (x y : atom) u e,
y <> x ->
lc u ->
open ([x ~> u] e) y = [x ~> u] (open e y).
This lemma states that opening can be replaced with variable
opening and substitution.
HINT: Prove by induction on e, first generalizing the argument to open_rec by using the generalize tactic, e.g., generalize 0.
HINT: Prove by induction on e, first generalizing the argument to open_rec by using the generalize tactic, e.g., generalize 0.
Lemma subst_intro : forall (x : atom) u e,
x `notin` (fv e) ->
open e u = [x ~> u](open e x).
End BasicOperations.
Cofinite quantification
Here we are stuck. We don't know that x0 is not in the free
variables of u.
The solution is to change the *definition* of local closure so that we get a different induction principle. Currently, in the lc_abs case, we show that an abstraction is locally closed by showing that the body is locally closed after it has been opened with one particular variable.
Therefore, our induction hypothesis in this case only applies to that variable. From the hypothesis list in the lc_abs case:
x0 : atom, IHHe : lc (x ~> uopen e x0)
The problem is that we don't have any assumptions about x0. It could very well be equal to x.
A stronger induction principle provides an IH that applies to many variables. In that case, we could pick one that is "fresh enough". To do so, we need to revise the above definition of lc and replace the type of lc_abs with this one:
This rule says that to show that an abstraction is locally closed, we need to show that the body is closed, after it has been opened by any atom x, *except* those in some set L. With this rule, the IH in this proof is now:
H0 : forall x0 : atom, x0 `notin` L -> lc (x ~> uopen e x0)
Below, lc_c is the local closure judgment revised to use this new rule in the abs case. We call this "cofinite quantification" because the IH applies to an infinite number of atoms x0, except those in some finite set L.
Changing the rule in this way does not change what terms are locally closed. (For more details about cofinite-quantification see: "Engineering Formal Metatheory", Aydemir, Chargu'eraud, Pierce, Pollack, Weirich. POPL 2008.)
The solution is to change the *definition* of local closure so that we get a different induction principle. Currently, in the lc_abs case, we show that an abstraction is locally closed by showing that the body is locally closed after it has been opened with one particular variable.
| lc_abs : forall (x : atom) e, x `notin` fv e -> lc (open e x) -> lc (abs e)
Therefore, our induction hypothesis in this case only applies to that variable. From the hypothesis list in the lc_abs case:
x0 : atom, IHHe : lc (x ~> uopen e x0)
The problem is that we don't have any assumptions about x0. It could very well be equal to x.
A stronger induction principle provides an IH that applies to many variables. In that case, we could pick one that is "fresh enough". To do so, we need to revise the above definition of lc and replace the type of lc_abs with this one:
| lc_abs_c : forall L e, (forall x:atom, x `notin` L -> lc (open e x)) -> lc (abs e)
This rule says that to show that an abstraction is locally closed, we need to show that the body is closed, after it has been opened by any atom x, *except* those in some set L. With this rule, the IH in this proof is now:
H0 : forall x0 : atom, x0 `notin` L -> lc (x ~> uopen e x0)
Below, lc_c is the local closure judgment revised to use this new rule in the abs case. We call this "cofinite quantification" because the IH applies to an infinite number of atoms x0, except those in some finite set L.
Changing the rule in this way does not change what terms are locally closed. (For more details about cofinite-quantification see: "Engineering Formal Metatheory", Aydemir, Chargu'eraud, Pierce, Pollack, Weirich. POPL 2008.)
Inductive lc_c : exp -> Prop :=
| lc_var_c : forall (x:atom),
lc_c x
| lc_abs_c : forall (L : atoms) e T,
(forall x : atom, x `notin` L -> lc_c (open e x)) ->
lc_c (abs T e)
| lc_app_c : forall e1 e2,
lc_c e1 ->
lc_c e2 ->
lc_c (app e1 e2).
Hint Constructors lc_c.
Section CofiniteQuantification.
Notation Local "{ k ~> u } t" := (open_rec k u t) (at level 67).
Lemma open_rec_lc_c : forall k u e,
lc_c e ->
e = {k ~> u} e.
Lemma subst_open_rec_c : forall e1 e2 u (x : atom) k,
lc_c u ->
[x ~> u] ({k ~> e2} e1) = {k ~> [x ~> u] e2} ([x ~> u] e1).
Lemma subst_open_var_c : forall (x y : atom) u e,
y <> x ->
lc_c u ->
open ([x ~> u] e) y = [x ~> u] (open e y).
Lemma subst_lc_c : forall (x : atom) u e,
lc_c e ->
lc_c u ->
lc_c ([x ~> u] e).
End CofiniteQuantification.
When picking a fresh atom or applying a rule that uses cofinite
quantification, choosing a set of atoms to be fresh for can be
tedious. In practice, it is simpler to use a tactic to choose the
set to be as large as possible.
The tactic gather_atoms is used to collect together all the atoms in the context. It relies on an auxiliary tactic, gather_atoms_with (from MetatheoryAtom), which maps a function that returns a finite set of atoms over all hypotheses with the appropriate type.
The tactic gather_atoms is used to collect together all the atoms in the context. It relies on an auxiliary tactic, gather_atoms_with (from MetatheoryAtom), which maps a function that returns a finite set of atoms over all hypotheses with the appropriate type.
Ltac gather_atoms ::=
let A := gather_atoms_with (fun x : atoms => x) in
let B := gather_atoms_with (fun x : atom => singleton x) in
let C := gather_atoms_with (fun x : list (atom * typ) => dom x) in
let D := gather_atoms_with (fun x : exp => fv x) in
constr:(A `union` B `union` C `union` D).
A number of other, useful tactics are defined by the Metatheory
library, and each depends on gather_atoms. By redefining
gather_atoms, denoted by the ::= in its definition below, we
automatically update these tactics so that they use the proper
notion of "all atoms in the context."
For example, the tactic (pick fresh x) chooses an atom fresh for "everything" in the context. It is the same as (pick fresh x for L), except where L has been computed by gather_atoms.
The tactic (pick fresh x and apply H) applies a rule H that is defined using cofinite quantification. It automatically instantiates the finite set of atoms to exclude using gather_atoms.
For example, the tactic (pick fresh x) chooses an atom fresh for "everything" in the context. It is the same as (pick fresh x for L), except where L has been computed by gather_atoms.
The tactic (pick fresh x and apply H) applies a rule H that is defined using cofinite quantification. It automatically instantiates the finite set of atoms to exclude using gather_atoms.
Example
Below, we reprove subst_lc_c using (pick fresh and apply). Step through the proof below to see how (pick fresh and apply) works.
We represent environments as association lists (lists of pairs of
keys and values) whose keys are atoms.
For STLC, environments bind atoms to typs. We define an
abbreviation env for the type of these environments. Coq will
print list (atom * typ) as env, and we can use env as a
shorthand for writing list (atom * typ).
Lists are defined in Coq's standard library, with the constructors nil and cons. The list library includes the :: notation for cons as well as standard list operations such as append, map, and fold. The infix operation "++" is list append.
The Metatheory library extends this reasoning by instantiating the AssocList library to provide support for association lists whose keys are atoms. Everything in this library is polymorphic over the type of objects bound in the environment. Look in AssocList for additional details about the functions and predicates that we mention below.
Lists are defined in Coq's standard library, with the constructors nil and cons. The list library includes the :: notation for cons as well as standard list operations such as append, map, and fold. The infix operation "++" is list append.
The Metatheory library extends this reasoning by instantiating the AssocList library to provide support for association lists whose keys are atoms. Everything in this library is polymorphic over the type of objects bound in the environment. Look in AssocList for additional details about the functions and predicates that we mention below.
Environment equality
When reasoning about environments, we often need to talk about
bindings in the "middle" of an environment. Therefore, it is common
for lemmas and definitions to use list append in their statements.
Unfortunately, list append is associative, so two Coq expressions may
denote the same environment even though they are not equal.
The tactic simpl_env reassociates all concatenations of environments to the right.
The tactic simpl_env reassociates all concatenations of environments to the right.
To make environments easy to read, instead of building them from
nil and cons, we prefer to build them from the following
components:
Furthermore, we introduce compact notation for one (singleton lists): (x ~ T) is the same as one (x, T).
- nil: The empty list.
- one: Lists consisting of exactly one item.
- ++: List append.
Furthermore, we introduce compact notation for one (singleton lists): (x ~ T) is the same as one (x, T).
The simpl_env tactic actually puts lists built from only nil, one
and ++ into a "normal form". This process reassociates all appends
to the right, removes extraneous nils converts cons to singleton
lists with an append.
Lemma simpl_env_demo : forall (x y:atom) (T1 T2:typ) (E F:env),
((x ~ T1) ++ nil) ++ (y,T2) :: (nil ++ E) ++ F =
(x ~ T1) ++ (y ~ T2) ++ E ++ F.
Note that the simpl tactic doesn't produce the "normal form" for
environments. It should always be followed up with simpl_env.
Furthermore, to convert an environment to any equivalent form other than the normal form (perhaps to apply a lemma) use the tactic rewrite_env.
Furthermore, to convert an environment to any equivalent form other than the normal form (perhaps to apply a lemma) use the tactic rewrite_env.
Lemma rewrite_env_demo : forall (x y:atom) (T:typ) P,
(forall E, P ((x,T):: E) -> True) ->
P (x ~ T) ->
True.
Environment operations.
The ternary predicate binds holds when a given binding is
present somewhere in an environment.
The function dom computes the domain of an environment,
returning a finite set of atoms. Note that we cannot use Coq's
equality for finite sets, we must instead use a defined relation
= for atom set equality.
The unary predicate uniq holds when each atom is bound at most
once in an environment.
The definition of the typing relation is straightforward. In
order to ensure that the relation holds for only well-formed
environments, we check in the typing_var case that the
environment is uniq. The structure of typing derivations
implicitly ensures that the relation holds only for locally closed
expressions. Finally, note the use of cofinite quantification in
the typing_abs case.
Inductive typing_c : env -> exp -> typ -> Prop :=
| typing_var_c : forall E (x : atom) T,
uniq E ->
binds x T E ->
typing_c E (fvar x) T
| typing_abs_c : forall (L : atoms) E e T1 T2,
(forall (x:atom), x `notin` L ->
typing_c ((x ~ T1) ++ E) (open e x) T2) ->
typing_c E (abs T1 e) (typ_arrow T1 T2)
| typing_app_c : forall E e1 e2 T1 T2,
typing_c E e1 (typ_arrow T1 T2) ->
typing_c E e2 T1 ->
typing_c E (app e1 e2) T2.
We add the constructors of the typing relation as hints to be used
by the auto and eauto tactics.
Hint Constructors typing_c.
Weakening states that if an expression is typeable in some
environment, then it is typeable in any well-formed extension of
that environment. This property is needed to prove the
substitution lemma.
As stated below, this lemma is not directly proveable. The natural way to try proving this lemma proceeds by induction on the typing derivation for e.
As stated below, this lemma is not directly proveable. The natural way to try proving this lemma proceeds by induction on the typing derivation for e.
Lemma typing_weakening_0 : forall E F e T,
typing_c E e T ->
uniq (F ++ E) ->
typing_c (F ++ E) e T.
We are stuck in the typing_abs_c case because the induction
hypothesis H0 applies only when we weaken the environment at its
head. In this case, however, we need to weaken the environment in
the middle; compare the conclusion at the point where we're stuck
to the hypothesis H, which comes from the given typing derivation.
We can obtain a more useful induction hypothesis by changing the statement to insert new bindings into the middle of the environment, instead of at the head. However, the proof still gets stuck, as can be seen by examining each of the cases in the proof below.
Note: To view subgoal n in a proof, use the command "Show n". To work on subgoal n instead of the first one, use the command "Focus n".
We can obtain a more useful induction hypothesis by changing the statement to insert new bindings into the middle of the environment, instead of at the head. However, the proof still gets stuck, as can be seen by examining each of the cases in the proof below.
Note: To view subgoal n in a proof, use the command "Show n". To work on subgoal n instead of the first one, use the command "Focus n".

The hypotheses in the typing_var_c case include an environment
E0 that that has no relation to what we need to prove. The
missing fact we need is that E0 = (G ++ E).
The problem here arises from the fact that Coq's induction tactic let's us only prove something about all typing derivations. While it's clear to us that weakening applies to all typing derivations, it's not clear to Coq, because the environment is written using concatenation. The induction tactic expects that all arguments to a judgement are variables. So we see E0 in the proof instead of (G ++ E).
The solution is to restate the lemma. For example, we can prove
The equality gets around the problem with Coq's induction tactic. The placement of the (forall G) quantifier gives us a sufficiently strong induction hypothesis in the typing_abs_c case.
However, we prefer not to state the lemma in the way shown above, since it is not as readable as the original statement. Instead, we use a tactic to introduce the equality within the proof itself. The tactic (remember t as t') replaces an object t with the identifier t' everywhere in the goal and introduces an equality t' = t into the context. It is often combined with generalize dependent, as illustrated below.
The problem here arises from the fact that Coq's induction tactic let's us only prove something about all typing derivations. While it's clear to us that weakening applies to all typing derivations, it's not clear to Coq, because the environment is written using concatenation. The induction tactic expects that all arguments to a judgement are variables. So we see E0 in the proof instead of (G ++ E).
The solution is to restate the lemma. For example, we can prove
forall E F E' e T, typing_c E' e T -> forall G, E' = G ++ E -> uniq (G ++ F ++ E) -> typing_c (G ++ F ++ E) e T.
The equality gets around the problem with Coq's induction tactic. The placement of the (forall G) quantifier gives us a sufficiently strong induction hypothesis in the typing_abs_c case.
However, we prefer not to state the lemma in the way shown above, since it is not as readable as the original statement. Instead, we use a tactic to introduce the equality within the proof itself. The tactic (remember t as t') replaces an object t with the identifier t' everywhere in the goal and introduces an equality t' = t into the context. It is often combined with generalize dependent, as illustrated below.
Exercise
See how we use remember as in the proof below for weakening. Then, complete the proof below.
HINTS:
- The typing_var_c case follows from binds_weaken, the weakening lemma for the binds relation.
- The typing_abs_c case follows from the induction hypothesis, but the apply tactic may be unable to unify things as you might expect.
-
- Recall the pick fresh and apply tactic.
-
- In order to apply the induction hypothesis, use rewrite_env to reassociate the list operations.
-
- After applying the induction hypothesis, use simpl_env to use uniq_push.
-
- Here, use auto to solve facts about finite sets of atoms, since it will simplify the dom function behind the scenes. fsetdec does not work with the dom function.
- The typing_app_c case follows directly from the induction hypotheses.
Lemma typing_c_weakening_strengthened : forall (E F G : env) e T,
typing_c (G ++ E) e T ->
uniq (G ++ F ++ E) ->
typing_c (G ++ F ++ E) e T.
Example
We can now prove our original statement of weakening. The only interesting step is the use of the rewrite_env tactic.
Lemma typing_c_weakening : forall (E F : env) e T,
typing_c E e T ->
uniq (F ++ E) ->
typing_c (F ++ E) e T.
Having proved weakening, we can now prove the usual substitution
lemma, which we state both in the form we need and in the
strengthened form needed to make the proof go through.
The proof of the strengthened statement proceeds by induction on the given typing derivation for e. The most involved case is the one for variables; the others follow from the induction hypotheses.
typing_c_subst_simple : forall E e u S T z, typing_c ((z ~ S) ++ E) e T -> typing_c E u S -> typing_c E ([z ~> u] e) T typing_c_subst : forall E F e u S T z, typing_c (F ++ (z ~ S) ++ E) e T -> typing_c E u S -> typing_c (F ++ E) ([z ~> u] e) T
The proof of the strengthened statement proceeds by induction on the given typing derivation for e. The most involved case is the one for variables; the others follow from the induction hypotheses.
Exercise
Below, we state what needs to be proved in the typing_var_c case of the substitution lemma. Fill in the proof.
Proof sketch: The proof proceeds by a case analysis on (x == z), i.e., whether the two variables are the same or not.
- If (x = z), then we need to show (typing (F ++ E) u T). This follows from the given typing derivation for u by weakening and the fact that T must equal S.
- If (x <> z), then we need to show (typing (F ++ E) x T). This follows by the typing rule for variables.
HINTS: Lemmas binds_mid_eq, uniq_remove_mid, and binds_remove_mid are useful.
Lemma typing_subst_var_case : forall (E F : env) u S T (z x : atom),
binds x T (F ++ (z ~ S) ++ E) ->
uniq (F ++ (z ~ S) ++ E) ->
typing_c E u S ->
typing_c (F ++ E) ([z ~> u] x) T.
Note
The other two cases of the proof of the substitution lemma are relatively straightforward. However, the case for typing_abs_c needs the fact that the typing relation holds only for locally-closed expressions.
Exercise
Complete the proof of the substitution lemma. The proof proceeds by induction on the typing derivation for e. The initial steps should use remember as and generalize dependent in a manner similar to the proof of weakening.
HINTS:
- Use the lemma proved above for the typing_var_c case.
- The typing_abs_c case follows from the induction hypothesis.
- Use simpl to simplify the substitution.
-
- Recall the tactic pick fresh and apply.
-
- In order to use the induction hypothesis, use subst_open_var_c to push the substitution under the opening operation.
-
- Recall the lemma typing_c_to_lc_c and the rewrite_env and simpl_env tactics.
- The typing_app_c case follows from the induction hypotheses. Use simpl to simplify the substitution.
Lemma typing_c_subst : forall (E F : env) e u S T (z : atom),
typing_c (F ++ (z ~ S) ++ E) e T ->
typing_c E u S ->
typing_c (F ++ E) ([z ~> u] e) T.
Exercise
Complete the proof of the substitution lemma stated in the form we need it. The proof is similar to that of typing_weakening.
HINT: You'll need to use rewrite_env to prepend nil, and simpl_env to simplify nil away.
Lemma typing_c_subst_simple : forall (E : env) e u S T (z : atom),
typing_c ((z ~ S) ++ E) e T ->
typing_c E u S ->
typing_c E ([z ~> u] e) T.
In order to state the preservation lemma, we first need to define
values and the small-step evaluation relation. These inductive
relations are straightforward to define.
Note the hypotheses which ensure that the relations hold only for locally closed terms. Below, we prove that this is actually the case, since it is not completely obvious from the definitions alone.
Note the hypotheses which ensure that the relations hold only for locally closed terms. Below, we prove that this is actually the case, since it is not completely obvious from the definitions alone.
Inductive value_c : exp -> Prop :=
| value_abs_c : forall e T1,
lc_c (abs T1 e) ->
value_c (abs T1 e).
Inductive eval_c : exp -> exp -> Prop :=
| eval_beta_c : forall e1 e2 T1,
lc_c (abs T1 e1) ->
value_c e2 ->
eval_c (app (abs T1 e1) e2) (open e1 e2)
| eval_app_1_c : forall e1 e1' e2,
lc_c e2 ->
eval_c e1 e1' ->
eval_c (app e1 e2) (app e1' e2)
| eval_app_2_c : forall e1 e2 e2',
value_c e1 ->
eval_c e2 e2' ->
eval_c (app e1 e2) (app e1 e2').
We add the constructors for these two relations as hints to be used
by Coq's auto and eauto tactics.
Hint Constructors value_c eval_c.
Take-home Exercise
Complete the proof of preservation. In this proof, we proceed by induction on the given typing derivation. The induction hypothesis has already been appropriately generalized by the given proof fragment.
Proof sketch: By induction on the typing derivation for e.
- typing_var_c case: Variables don't step.
- typing_abs_c case: Abstractions don't step.
- typing_app_c case: By case analysis on how e steps. The eval_beta case is interesting, since it follows by the substitution lemma. The others follow directly from the induction hypotheses.
Exercise
Complete the proof of the progress lemma. The induction hypothesis has already been appropriately generalized by the given proof fragment.
Proof sketch: By induction on the typing derivation for e.
- typing_var_c case: Can't happen; the empty environment doesn't bind anything.
- typing_abs_c case: Abstractions are values.
- typing_app_c case: Applications reduce. The result follows from an exhaustive case analysis on whether the two components of the application step or are values and the fact that a value must be an abstraction.
Lemma typing_c_uniq : forall E e T,
typing_c E e T -> uniq E.
Lemma typing_c_rename : forall (x y : atom) E e T1 T2,
x `notin` fv e -> y `notin` (dom E `union` fv e) ->
typing_c ((x ~ T1) ++ E) (open e x) T2 ->
typing_c ((y ~ T1) ++ E) (open e y) T2.
Inductive typing : env -> exp -> typ -> Prop :=
| typing_var : forall E (x : atom) T,
uniq E ->
binds x T E ->
typing E (fvar x) T
| typing_abs : forall E e T1 T2 (x : atom),
x `notin` fv e ->
typing ((x ~ T1) ++ E) (open e x) T2 ->
typing E (abs T1 e) (typ_arrow T1 T2)
| typing_app : forall E e1 e2 T1 T2,
typing E e1 (typ_arrow T1 T2) ->
typing E e2 T1 ->
typing E (app e1 e2) T2.
Inductive value : exp -> Prop :=
| value_abs : forall e T1,
lc (abs T1 e) ->
value (abs T1 e).
Inductive eval : exp -> exp -> Prop :=
| eval_beta : forall e1 e2 T1,
lc (abs T1 e1) ->
value e2 ->
eval (app (abs T1 e1) e2) (open e1 e2)
| eval_app_1 : forall e1 e1' e2,
lc e2 ->
eval e1 e1' ->
eval (app e1 e2) (app e1' e2)
| eval_app_2 : forall e1 e2 e2',
value e1 ->
eval e2 e2' ->
eval (app e1 e2) (app e1 e2').
Hint Constructors typing value eval.
First, we show that the two local closure predicates are equivalent.
This lemma follows via a renaming lemma for lc_c.
Lemma lc_rename : forall e (x:atom) (y:atom),
x `notin` fv e ->
lc_c (open e x) -> lc_c (open e y).
Lemma lc_to_lc_c : forall e, lc e -> lc_c e.
Lemma lc_c_to_lc : forall e, lc_c e -> lc e.
x `notin` fv e ->
lc_c (open e x) -> lc_c (open e y).
Lemma lc_to_lc_c : forall e, lc e -> lc_c e.
Lemma lc_c_to_lc : forall e, lc_c e -> lc e.
Correspondence of typing and typing_c
Lemma typing_to_typing_c : forall E e T,
typing E e T -> typing_c E e T.
Lemma typing_c_to_typing : forall E e T,
typing_c E e T -> typing E e T.
Lemma value_to_value_c : forall e,
value e -> value_c e.
Lemma value_c_to_value : forall e,
value_c e -> value e.
Lemma eval_to_eval_c : forall e e',
eval e e' -> eval_c e e'.
Lemma eval_c_to_eval : forall e e',
eval_c e e' -> eval e e'.
Lemma preservation : forall E e e' T,
typing E e T ->
eval e e' ->
typing E e' T.
Lemma progress : forall e T,
typing nil e T ->
value e \/ exists e', eval e e'.
To be fully confident about the exist-fresh rules, we can show their
"regularity" --- that these relations only include locally closed
terms. (For the exists-fresh definition of local closure.)
Importantly: to prove regularity, we need to know subst_lc, and that
we most directly prove by using the connection between lc and lc_c.
Take-home exercise. open_abs is the analogue of subst_lc for bound variable
substitution.
HINT: use inversion, subst_intro and subst_lc to prove this lemma.
Lemma open_abs : forall e u T1,
lc (abs T1 e) ->
lc u ->
lc (open e u).
Lemma value_to_lc : forall e,
value e -> lc e.
Lemma eval_to_lc : forall e1 e2,
eval e1 e2 -> lc e1 /\ lc e2.
Lemma typing_to_lc : forall E e T,
typing E e T -> lc e.
lc (abs T1 e) ->
lc u ->
lc (open e u).
Lemma value_to_lc : forall e,
value e -> lc e.
Lemma eval_to_lc : forall e1 e2,
eval e1 e2 -> lc e1 /\ lc e2.
Lemma typing_to_lc : forall E e T,
typing E e T -> lc e.
Equality on types is decidable
Take-home exercise.
To prove that ill-formed terms cannot be typechecked, we will need an auxiliary lemma that says that each term only has a single type.
HINT: to prove this lemma you will need to generalize the induction hypothesis for T2 and use the lemma binds_unique from AtomEnv.v.
To prove that ill-formed terms cannot be typechecked, we will need an auxiliary lemma that says that each term only has a single type.
HINT: to prove this lemma you will need to generalize the induction hypothesis for T2 and use the lemma binds_unique from AtomEnv.v.
Lemma typing_c_unique : forall E e T1 T2,
typing_c E e T1 ->
typing_c E e T2 ->
T1 = T2.
Definition decidable (P : Prop) := (P \/ ~ P).
Lemma typing_c_decidable : forall E e,
lc_c e -> uniq E -> decidable (exists T, typing_c E e T).
Check (typing_abs_c L E (abs T e) T S).
Qed.

Definition decidable (P : Prop) := (P \/ ~ P).
Lemma typing_c_decidable : forall E e,
lc_c e -> uniq E -> decidable (exists T, typing_c E e T).
Check (typing_abs_c L E (abs T e) T S).
Qed.

This page has been generated by coqdoc


Commune functions
This page only available to the Commune Account
New Budget Goals
Goal Demurrage income:
Goal Crowd-funding income:
Goal Service Hours spending:
Goal Expenses spending:
Change Budget Goals
Change Treasury address
Change Treasury address
Accept new Commoner
Account
Alias
Accept
Remove Commoner
Account:
Remove
Attribute Reputation
Account:
Reputation in UoT:
Attribute reputation


To import a list of products two files are needed: a TSV (tab seperated) text
file that contains information on the products to be imported and (optionaly) a
zip file containing the design files.
The following headers are valid for use in the product information file. Those
marked with an asterix (*) are required: name*, status*, product_type*,
optimised_for.
All information supplied must match a valid input for the corrosponding field or
it will be rejected. Some values are case sensitive, using the incorrect case
will cause the entry to be rejected.


A loader for `LDraw` resources.
[link:https://ldraw.org LDraw] (LEGO Draw) is an
[link:https://ldraw.org/article/218.html open format specification] for describing LEGO
and other construction set 3D models.
An LDraw asset (a text file usually with extension .ldr, .dat or .txt) can describe just a single construction piece, or an entire model. In the case of a model the LDraw file can reference other LDraw files, which are loaded from a library path set with [page:Function setPartsLibraryPath]. You usually download the LDraw official parts library, extract to a folder and point setPartsLibraryPath to it.
Library parts will be loaded by trial and error in subfolders 'parts', 'p' and 'models'. These file accesses are not optimal for web environment, so a script tool has been made to pack an LDraw file with all its dependencies into a single file, which loads much faster. See section 'Packing LDraw models'. The LDrawLoader example loads several packed files. The official parts library is not included due to its large size.
[name] is an add-on, and must be imported explicitly. See [link:#manual/introduction/Installation Installation / Addons].
import { LDrawLoader } from 'three/addons/loaders/LDrawLoader.js';
LDrawLoader supports the following extensions:
// Instantiate a loader
const loader = new LDrawLoader();
// Optionally set library parts path
// loader.setPartsLibraryPath( path to library );
// Load a LDraw resource
loader.load(
// resource URL
'models/car.ldr_Packed.mpd',
// called when the resource is loaded
function ( group ) {
// Optionally, use LDrawUtils.mergeObject() from
// 'examples/jsm/utils/LDrawUtils.js' to merge all
// geometries by material (it gives better runtime
// performance, but building steps are lost)
// group = LDrawUtils.mergeObject( group );
scene.add( group );
},
// called while loading is progressing
function ( xhr ) {
console.log( ( xhr.loaded / xhr.total * 100 ) + '% loaded' );
},
// called when loading has errors
function ( error ) {
console.log( 'An error happened' );
}
);
[example:webgl_loader_ldraw]
To pack a model with all its referenced files, download the [link:https://www.ldraw.org/parts/latest-parts.html Official LDraw parts library] and use the following Node script: [link:https://github.com/mrdoob/three.js/blob/master/utils/packLDrawModel.js utils/packLDrawModel.js] It contains instructions on how to setup the files and execute it.
LDrawLoader returns a [page:Group] object which contains an object hierarchy. Depending of each subobject
type, its .userData member will contain the following members:
In a [page:Group], the userData member will contain:
In a [page:Material], the userData member will contain:
[page:LoadingManager manager] — The [page:LoadingManager loadingManager] for the loader to use. Default is [page:LoadingManager THREE.DefaultLoadingManager].
Creates a new [name].
See the base [page:Loader] class for common properties.
See the base [page:Loader] class for common methods.
[page:String url] — A string containing the path/URL of the LDraw file.
[page:Function onLoad] — A function to be called after the loading is successfully completed. The function receives the loaded JSON response returned from [page:Function parse].
[page:Function onProgress] — (optional) A function to be called while the loading is in progress. The argument will be the XMLHttpRequest instance, that contains .[page:Integer total] and .[page:Integer loaded] bytes. If the server does not set the Content-Length header; .[page:Integer total] will be 0.
[page:Function onError] — (optional) A function to be called if an error occurs during loading. The function receives error as an argument.
Begin loading from url and call the callback function with the parsed response content.
[page:String path] — Path to library parts files to load referenced parts from. This is different from [page:Loader.setPath], which indicates the path to load the main asset from.
This method must be called prior to [page:.load] unless the model to load does not reference library parts (usually it will be a model with all its parts packed in a single file)
[page:Map map] — Set a map from [page:String] to [page:String] which maps referenced library filenames to new filenames. If a fileMap is not specified (the default), library parts will be accessed by trial and error in subfolders 'parts', 'p' and 'models'.
[page:String text] — LDraw asset to parse, as string.
[page:String path] — The base path from which to find other referenced LDraw asset files.
[page:Function onLoad] — A function to be called when parse completes.
Parse a LDraw file contents as a String and fire [page:Function onLoad] callback when complete. The argument to [page:Function onLoad] will be an [page:Group] that contains hierarchy of [page:Group], [page:Mesh] and [page:LineSegments] (with other part data in .userData fields).
[page:String colourCode] — Color code to get the associated [page:Material].
Returns the [page:Material] for the main LDraw color.
For an already loaded LDraw asset, returns the [page:Material] associated with the main color code. This method can be useful to modify the main material of a model or part that exposes it.
The main color code is the standard way to color an LDraw part. It is '16' for triangles and '24' for edges. Usually a complete model will not expose the main color (that is, no part uses the code '16' at the top level, because they are assigned other specific colors) An LDraw part file on the other hand will expose the code '16' to be colored, and can have additional fixed colors.
Returns the [page:Material] for the edges main LDraw color.
[page:String path] — Path of the LDraw materials asset.
This async method preloads materials from a single LDraw file. In the official parts library there is a special file which is loaded always the first (LDConfig.ldr) and contains all the standard color codes. This method is intended to be used with not packed files, for example in an editor where materials are preloaded and parts are loaded on demand.
[link:https://github.com/mrdoob/three.js/blob/master/examples/jsm/loaders/LDrawLoader.js examples/jsm/loaders/LDrawLoader.js]


Japanese hotel group Unizo gets six new buyout offers
TOKYO (Reuters) - Japanese hotel operator Unizo Holdings (3258.T) said on Sunday it had received six more buyout offers at a price competitive with an existing $1.6 billion bid proposed by Blackstone Group (BX.N).
Unizo said it had received offers from four overseas investment funds and one Japanese fund as well as one domestic company, without naming the bidders.
Unizo said none of the offers would meet its demands.
The multiple offers may further complicate the takeover saga surrounding the hotel operator, which is already in talks with two top global investment groups - Blackstone and Fortress Investment Group.
Unizo in July became a target for a hostile bid by a Japanese travel agent H.I.S. Co (9603.T). Unizo at one stage turned to SoftBank Group-owned (9984.T) Fortress to fend off the bid. But later it withdrew its support for Fortress’ white-knight offer.
Last month, Blackstone offered to buy the company at 5,000 yen per share, valuing Unizo at $1.6 billion.
Unizo said on Sunday it was positively engaged in talks with Blackstone. Blackstone on Friday extended the deadline for Unizo to respond to its offer..
Fortress is currently running a public tender offer to buy Unizo at 4,100 yen per share, valuing the company at $1.3 billion. Unizo said on Sunday it was asking Fortress to raise its bid price to 5,000 yen per share. Unizo said it wanted any bidder to make an offer at 5,000 yen per share or more. Some of the new bidders are still considering the offer price, Unizo said.


Using DSRM Credentials over the network
It is possible to use the DSRM Credentials over the network.
When Windows 2000 and Active Directory were released, DSRM being limited to console logon was a good security method. Today, however, there are several methods to logon to a system “at the console”:
Virtualization Client
VMWare Remote Console (TCP 903)
Hyper-V VM Connection (TCP 5900)
Out of Band Management (Lights Out, etc)
Network KVM
Remote Desktop Client when connecting to the “Console” which is “mstsc /console” prior to Windows Server 2008 and “mstsc /admin” with Windows Server 2008 and newer. Tested on Windows Server 2008 R2. Windows Server 2012R2 seems to refuse DSRM logon via RDP console.
Once logged in as the local DC’s DSRM account (DC local admin), we can confirm we are on a DC and that this is the DC’s local administrator account. not a domain account.
If DsrmAdminLogonBehavior regkey is set to 2, you can pass the hash with the DSRM hash


THE STRAIGHT STORY (Disney) Starring: Richard Farnsworth, Sissy Spacek, Everett McGill, John Farley, Jennifer Edwards-Hughes, Harry Dean Stanton. Screenplay: John Roach and Mary Sweeney. Producers: Mary Sweeney and Neil Edelstein. Director: David Lynch. MPAA Rating: G (mild profanity) Running Time: 111 minutes. Reviewed by Scott Renshaw.
In most exceptional films, there is a moment early on when you can just tell you're tapped into something special. That moment in THE STRAIGHT STORY comes as Alvin Straight (Richard Farnsworth), a 73-year-old widower with failing eyesight and failing hips, begins the true-story trek at the center of the film. Having recently learned that his estranged brother Lyle has had a stroke, Alvin decides it's time to make amends. He sets out from his home in Laurens, Iowa to Lyle's home in Mt. Zion, Wisconsin on the only transportation at his disposal: a riding lawnmower. As Alvin hits the two-lane highway, director David Lynch slowly pans up from Alvin to the cloud-filled sky above the Iowa fields. He holds that shot for what seems like a full minute, then slowly pans back down... where we see Alvin's puttering rig about 100 yards from where we last saw it.
I think that shot might have been one of the best of the year even if its only purpose had been as a shaggy dog joke. But it's more than that; it's a remarkably efficient tone-setter. Instantly, you know this is going to be a rather unique travelogue. You can begin to appreciate the truly inspired combination of Freddie Francis's cinematography and Angelo Badalamenti's fiddle-and-guitar road music that makes THE STRAIGHT STORY so evocative in its heartland sincerity. And you understand that slow, methodical persistence is central to this story's success -- not just in Alvin's journey, but in Lynch's willingness to ask his audience for some patience as the film unfolds.
If you're busy rubbing your eyes incredulously, wondering if we could possibly be talking about the same David Lynch who made "Twin Peaks," BLUE VELVET and LOST HIGHWAY, let me assure you that we are. We're also talking about the same David Lynch who made THE ELEPHANT MAN, another fact-based story overflowing with compassion and humanity. There may be something about working from real life that keeps Lynch anchored, and it's a style that suits him well. As provocative as his more surreal films have been, they can make it difficult to appreciate what a talented director he is between the cringes and the head-scratching. In THE STRAIGHT STORY, he is more in command of his simple visual storytelling than he has ever been, which is not necessarily saying that THE STRAIGHT STORY is his best film. It's simply obvious, with none of the grotesquerie characteristic of other Lynch films, that he knows exactly what works for any given story.
He also knows that THE STRAIGHT STORY is more than a bunch of pretty pictures of the American midwest. Richard Farnsworth's performance is so low-key and naturalistic that it may not seem there's a lot going on, but Alvin Straight is a superbly crafted character. Senior citizens rarely get the kind of showcase THE STRAIGHT STORY provides, and Farnsworth does beautiful things with Alvin. It's always clear that he's a stubborn man, but it becomes clear that he's also a man trying to make the wisdom of his years mean something. His journey to reconcile with Lyle becomes a chance to show he's learned what matters, and that difficult moments in life can be overcome by one selfless act. If you're unmoved by Lyle's (Harry Dean Stanton) silent realization of what Alvin has done for him, then movies may hold no power to move you.
It's true that Alvin's homespun homilies -- to a teenage runaway he encounters; to young cyclists; to the feuding twins who fix his lawnmower -- do drag THE STRAIGHT STORY down a bit. Farnsworth does a fine job of pulling all possible sanctimony out of those scenes, but the film is still stronger when it's quiet and observant, soaring on the skills of Francis and Badalamenti. There's also a sly sense of humor to THE STRAIGHT STORY, including Lynch's ability to poke fun at himself. In a very early scene, he trains his camera on a front yard, where a heavy-set woman lies tanning herself. It's exactly the kind of scene where Lynch might have dipped into the creatures beneath the green lawn, or found some other bit of suburban horror. In THE STRIAGHT STORY, he just tells a straight story, finding poetry in the simple reliability of a lawnmower's slow, steady journey.
On the Renshaw scale of 0 to 10 mow better blues: 9.
Visit Scott Renshaw's Screening Room http://www.inconnect.com/~renshaw/ *** Subscribe to receive new reviews directly by email! See the Screening Room for details, or reply to this message with subject "Subscribe".
The review above was posted to the
rec.arts.movies.reviews newsgroup (de.rec.film.kritiken for German reviews).
The Internet Movie Database accepts no responsibility for the contents of the
review and has no editorial control. Unless stated otherwise, the copyright
belongs to the author.
Please direct comments/criticisms of the review to relevant newsgroups.
Broken URLs inthe reviews are the responsibility of the author.
The formatting of the review is likely to differ from the original due
to ASCII to HTML conversion.
Related links: index of all rec.arts.movies.reviews reviews


{{object.client.name}} {{object.project.name}} {{object.date}} Time spent: {{object.time_spent}} Note: {{object.notes}} Expenses: {{object.expenses}} Note: {{object.expense_notes}} Miles: {{object.miles}} Note: {{object.miles_notes}} EDIT DELETE


This section explains how the value returned by a Java extension function is converted to an XPath value. The same rules are used in converting a Java object supplied as a parameter to a stylesheet or query.
The result type of the method is converted to an XPath value as follows.
If the method returns void, the XPath value is an empty sequence.
If the method returns null, the XPath value is an empty sequence.
If the method is a constructor, the XPath value is of type "wrapped Java object". The only way of using this is by passing it to another external function, or by converting it to one of the standard XPath data types as described above.
If the returned value is a Java boolean or Boolean, the XPath result is a boolean.
If the returned value is a Java double or Double, the XPath result is a double.
If the returned value is a Java float or Float, the XPath result is a float.
If the returned value is a Java int, short, long, character, or byte, or one of their object wrapper equivalents, the XPath result is an integer.
If the returned value is a Java String, the XPath result is a string.
If the returned value is an instance of the Saxon class net.sf.saxon.om.NodeInfo
(a node in a Saxon tree), the XPath value will be a sequence containing a single node.
If the returned value is an instance of javax.xml.transform.Source
(other than a NodeInfo
),
a tree is built from the specified Source
object, and the root node of this tree is returned as
the result of the function.
If the returned value is an instance of the Saxon class net.sf.saxon.value.Value
,
the returned value is used unchanged.
If the returned value is is an instance of the Saxon class net.sf.saxon.om.SequenceIterator
(an iterator over a sequence), the XPath
value will be the sequence represented by this iterator. It is essential that this iterator
properly implements the method getAnother()
which returns a new iterator over the
same sequence of nodes or values, positioned at the start of the sequence.
If the returned value is an instance of the Java class java.util.List
, or if it is an array,
the XPath value will be the
sequence represented by the contents of this List
or array. The members of the list or array
will each be converted
to an XPath value, as if each member was supplied from a separate function call. An error is reported if
the result contains a list or array nested within another list or array.
The contents of the list or array are copied immediately on return from the
function, so the original List
or array object itself may be safely re-used.
If the returned value is a DOM NodeList
, the list of nodes is returned as a Saxon node-set. However,
all the nodes must be instances of class net.sf.saxon.om.NodeInfo
, that is, they must use Saxon's tree
implementation, not some third-party DOM. But any implementation of NodeList
can be used. The nodes
can come from the original source tree, or from a newly-constructed tree, so long as it is constructed
using Saxon.
If the returned value is a DOM Node that is not an instance of class net.sf.saxon.om.NodeInfo
, it is
rejected: the result must use Saxon's DOM implementation, not some third-party DOM.
If the result is any other Java object (including null), it is returned as a "wrapped Java object".
Note that Saxon's two principal tree structures both conform to the DOM Core Level 2 interface. However, they are read-only:
any attempt to modify the tree causes an exception. Saxon's trees can only be built using the Saxon
subclasses of the net.sf.saxon.tree.Builder
class, and they cannot be modified in situ.
(The simplest way for a Java application to build a Saxon tree is by
using the net.sf.saxon.xpath.XPathEvaluator
class.)
In XSLT, the system function function-available(String name)
returns true if there appears
to be a method available with the right name. The function also has an optional second argument to test whether
there is a method with the appropriate
number of arguments. However, it is not possible to test whether the arguments are of appropriate types.
If the function name is "new" it
returns true so long as the class is not an abstract class or interface, and so long as it has at least
one constructor.
There are a number of extension functions supplied with the Saxon product: for details, see
extensions.html. The source code of these methods, which
in most cases is extremely simple, can be used as an example for writing
other user extension functions. It is found in class net.sf.saxon.functions.Extensions
.


If you know the name or "code" of a
previously saved mad lib you can enter it here to retrieve the clues for that mad lib, fill them out, then see the completed mad lib.
This performs a Hard Refresh of the page. I.e. It resets all fields back to their initial values.
Write your mad lib:
The text area below this statement is where you can write your own mad lib. It comes pre-filled with an example;
notice that the words that are to be replaced are in [brackets] and they describe a type of word. You MUST USE [brackets]
to denote replaceable words or else your mad lib will not work.
Once you've written a mad lib, you can save it.
You cannot use a name that someone else has already used, so try to choose a unique name.
Once you've saved it, anyone can access it using the button if they have the name. (Bear in mind that
what you write is not necessarily private and could possibly be accessed by people other than your intended audience,
so please don't write anything too profane, disturbing, or creepy. If you do and I happen to see it, I will probably delete it.)
Once you've written your mad lib, if you are ready to play it,
click this button to go to the filling-out-the-words part.
Fill in your words:
This appears at the top of the filling-out-the-words window. There are fields for you to
-you guessed it- fill out the words!
This button is at the bottom of the filling-out-the-words window.
Click it once you've filled in the words to see what your mad lib says!


Russell, Langevine lead Rhode Island past Nicholls St. 70-65
by EndPlayKINGSTON, R.I. (AP) - Fatts Russell had 22 points, six assists and five steals, Cyril Langevine had a double-double, and Rhode Island beat Nicholls State 70-65 on Tuesday night.
Langevine finished with 10 points and 11 rebounds and Jermaine Harris also scored 10 points for Rhode Island.
The game featured 15 ties and 10 the lead changes, the last of which came when Tyrese Martin hit a 3-pointer that made it 63-62 with 1:46 to play. Warith Alatishe made 1-of-2 free throws to tie it 17 seconds later but Langevine converted a three-point play and, after a turnover by Alatishe, Russell made an acrobatic double-clutch layup to give the Rams (3-1) a 68-63 lead with 45 seconds remaining. Russell added two free throws before Alatishe's layup with eight seconds left capped the scoring.
Alatishe scored 17 points and grabbed 10 rebounds - both career highs - and had a career-best tying five steals. Andre Jones added 16 points and Dexter McClanahan 15 for Nicholls State (2-3).
Russell made all his career-high nine foul shots and Rhode Island outscored the Colonels 19-5 from the free-throw line.
___
For more AP college basketball coverage: https://apnews.com/Collegebasketball and http://twitter.com/AP_Top25
___
Elements of this story were generated by Automated Insights, http://www.automatedinsights.com/ap, using data from STATS LLC, https://www.stats.com


| Figure 1 |
The distribution of malaria cases according to the continent ... |
| Figure 2 |
The distribution of malaria cases according to the age facto ... |
| Figure 3 |
The distribution of malaria cases according to the strain of ... |
| Figure 4 |
The distribution of malaria cases according to the travel pu ... |
| Figure 5 |
The distribution of malaria cases recorded in Romania betwee ... |
| Figure 6 |
The evolution of the annual maximum temperature, the average ... |
| Figure 7 |
The average annual temperature and the average temperature c ... |
| Figure 8 |
The monthly average temperatures calculated according to dec ... |
| Figure 9 |
The map of the average temperatures calculated for the month ... |
| Figure 10 |
The map of the estimated temperatures for July, for the year ... |


Book for Navigating Parks
Rwanda: 3000Rwf/person
EAC: 5000Rwf/person
Foregners:10,000Rwf/person
Transportation:30,000rwf
Booking for Hotels
Booking for Culture Exporation
Rwanda: 4000Rwf/person
EAC: 6000Rwf/person
Foregners:12,000Rwf/person
Transportation:30,000rwf
Booking for History learning
Rwanda: 2000Rwf/person
EAC: 3000Rwf/person
Foregners:9,000Rwf/person
Transportation:10,000rwf
Your Name :
Your Email :
Name of Hotel :
The type OF Hotel:
Number of Visitors :
Arrival Date :
Arrival Time :
Depature Date :
Depature Time :
Free Pick Up:
Special Request:
Your Price :
Transport:
Number of Visitors :
Total:
Price :
Transport:
Number of Visitors :
Total:
Price :
Transport:
Number of Visitors :
Total:


A monad is a monoid in the category of endofunctors, what's the problem?
let numbers = [1, ...]
fun is_prime x = all (map (y -> x mod y <> 0) [2..x-1])
let primes = filter is_prime numbers
let tenth_prime = first (take primes 10)
print tenth_prime
if user.signed_in? && user.current_order&.pending?
# ...
f = Future.new do
# executed asynchronously
end
f.complete? # non-blocking
f.on_complete do |value|
# called upon completion; preferred approach
end
f.value # blocks until complete; less preferred approach
users = UsersService.all
archived_users = ArchivedUsersService.for_last_month
(users + archived_users).select(&:active?).size
count(
only_active(
concat(
Future.new { UsersService.all },
Future.new { ArchivedUsersService.for_last_month }
)
)
)
count_f(
only_active_f(
concat_f(
Future.new { UsersService.all },
Future.new { ArchivedUsersService.for_last_month }
)
)
)
(aka "bind", "return")
f = Future.new(x)
# or
f = Future.new
f.complete_with(x)
f.value # doesn't block
f.complete? # == true
class Future
# unit : Value -> Future<Value>
def self.unit(value)
Future.new(value)
end
end
# count_f : Future<Enumerable> -> Future<Integer>
def count_f(future)
future.fmap(
# f: Enumerable -> Integer
->(enumerable) { enumerable.count }
)
end
class Future
# ...
# fmap: Func<Value, Value> -> Future<Value>
def fmap(func)
f_new = Future.new
on_complete do |value|
f_new.complete_with(func.call(value))
end
f_new
end
end
# only_active_f : Future<Enumerable> -> Future<Enumerable>
def only_active_f(future)
future.fmap(
# f: Enumerable -> Enumerable
->(enumerable) { enumerable.select(&:active?) }
)
end
f = Future.new { UsersService.all }.fmap(
# f: Enumerable -> Future<Profile>
->(users) {
Future.new { ProfileService.profile_for(users.first) }
}
)
f.value # let's get the profile of a first user...
oops...
class Future
def fmap(func)
f_new = Future.new
on_complete do |value|
f_new.complete_with(func.call(value)) # it's a Future!
end
f_new
end
end
(aka "join")
class Future
# ...
protected
# flatten: Future<Future<Value>> -> Future<Value>
def flatten
f_flat = Future.new
on_complete do |f_internal|
f_internal.on_complete do |value|
f_flat.complete_with(value)
end
end
f_flat
end
end
(aka "flatMap")
class Future
# ...
# bind: Func<Value, Future<Value>> -> Future<Value>
def bind(func)
fmap(func).flatten
end
end
f = Future.new { UsersService.all }.bind(
# f: Enumerable -> Future<Profile>
->(users) {
Future.new { ProfileService.profile_for(users.first) }
}
)
# fmap(func).flatten was called under the hood
f.value # now it's the Profile
concat_f
function
count -> lift -> count_f
def lift(func)
->(future) { future.fmap(func) }
end
concat -> lift2 -> concat_f
# Func<Value, Value, Value>
# -> Func<Future<Value>, <Future<Value>, <Future<Value>>
def lift2(func) # aka "liftM2"
# ...
end
unit
operation defined which wraps a value in it
bind
operation defined which allows building a chain of transformations over a monadic value
All of these make monad a "programmable semicolon"
class Maybe
attr_reader :value
class Some < Maybe
def initialize(value)
@value = value
end
end
class None < Maybe; end
end
class Maybe
# "unit" function
def self.[](value)
value.nil? ? None.new : Some.new(value)
end
def bind(func)
is_a?(None) ? self : func.call(self.value)
end
alias_method :>=, :bind
end
# add_m2:
# Func<Maybe<Integer>, Maybe<Integer>> -> Maybe<Integer>
def add_m2(m1, m2)
m1.>=( # calling bind
->(x) { # in binding function; value of m1 unpacked to x
# we need to return Maybe from here; m2 is Maybe
# m2.>= will also return Maybe
m2.>=( # calling bind
->(y) { # value of m2 unpacked to y
Maybe[x + y] # x and y are Integers
# add them and wrap the result into Maybe
}
)
}
)
end
add_m2(Maybe[1], Maybe[2]) # => Maybe::Some#<value = 3>
add_m2(Maybe[4], Maybe[5]).value # => 9
add_m2(Maybe[nil], Maybe[5])
# => Maybe::None; "bind" of Maybe[5] was not executed
maybe_user = Maybe(user).bind do |u|
Maybe(u.address).bind do |a|
Maybe(a.street)
end
end
# If user with address exists
=> Some("Street Address")
# If user or address is nil
=> None()
def calculate(input)
Right(input).bind do |value|
value > 1
? Right(value + 3)
: Left("value was less than 1")
end.bind do |value|
value % 2 == 0
? Right(value * 2)
: Left("value was not even")
end
end
calculate(3) # => Right(12)
calculate(0) # => Left("value was less than 1")
calculate(0).value # => "value was less than 1"
res = Try() { 10 / 2 }
res.value if res.success?
# => 5
res = Try() { 10 / 0 }
res.exception if res.failure?
# => #<ZeroDivisionError: divided by 0>
Try(NoMethodError, NotImplementedError) { 10 / 0 }
# => raised ZeroDivisionError: divided by 0 exception
Remember, you can always write your own
Questions?


THE WEDDING SINGER (1998)
Rating: 2.5 stars (out of 4.0) ******************************** Key to rating system: 2.0 stars - Debatable 2.5 stars - Some people may like it 3.0 stars - I liked it 3.5 stars - I am biased in favor of the movie 4.0 stars - I felt the movie's impact personally or it stood out ********************************* A Movie Review by David Sunga
Directed by: Frank Coraci
Written by: Tim Herlihy
Starring: Adam Sandler, Drew Barrymore, Christine Taylor, Matthew Glave
Ingredients: 1980s setting, wedding musician, waitress, romance
Synopsis: The story takes place in the 1980s but it could just as easily be any typical Hollywood romantic comedy where boy meets girl, boy loses girl, and they regain each other by the end. Robbie (Adam Sandler) is a down and out musician who makes his living singing at weddings. After getting left at the altar at his own wedding, Robbie's luck goes downhill until he falls in love with his friend, a waitress named Julia (Drew Barrymore). The two were made for each other.  At the same time, Robbie's scummy old fiancee wants to get back together with him. Can Robbie and Julia get past all the misunderstandings and find true love with each other before Julia takes that plane to Vegas to marry Glen?
 Although it is silly at times, and neither deep nor meaningful THE WEDDING SINGER is big-hearted happy movie that any sucker for romance would love to watch.
Reviewed by David Sunga February 13, 1998
Copyright © 1998 This review and others like it can be found at THE CRITIC ZOO: http://www.criticzoo.com email<EMAIL_ADDRESS>The review above was posted to the
rec.arts.movies.reviews newsgroup (de.rec.film.kritiken for German reviews).
The Internet Movie Database accepts no responsibility for the contents of the
review and has no editorial control. Unless stated otherwise, the copyright
belongs to the author.
Please direct comments/criticisms of the review to relevant newsgroups.
Broken URLs inthe reviews are the responsibility of the author.
The formatting of the review is likely to differ from the original due
to ASCII to HTML conversion.
Related links: index of all rec.arts.movies.reviews reviews


@{ set . "title" "Oops !" }@ @{ template "header.html" .}@ @{ if eq .RunMode "dev" }@ @{ template "errors/500-dev.html" . }@ @{ else }@
This exception has been logged.


NAME
load_resource_usage.pl
DESCRIPTION
This script obtains resource usage data for your pipeline from the Meadow and stores it in 'worker_resource_usage' table.
Your Meadow class/plugin has to support offline examination of resources in order for this script to work.
Based on the start time of the first Worker and end time of the last Worker (as recorded in pipeline DB),
it pulls the relevant data out of your Meadow (runs 'bacct' script in case of LSF), parses the report and stores in 'worker_resource_usage' table.
You can join this table to 'worker' table USING(meadow_name,process_id) in the usual MySQL way
to filter by analysis_id, do various stats, etc.
You can optionally provide an an external filename or command to get the data from it (don't forget to append a '|' to the end!)
and then the data will be taken from your source and parsed from there.
USAGE EXAMPLES
# Just run it the usual way: query and store the relevant data into 'worker_resource_usage' table:
load_resource_usage.pl -url mysql://username:secret@hostname:port/long_mult_test
# The same, but assuming another user 'someone_else' ran the pipeline:
load_resource_usage.pl -url mysql://username:secret@hostname:port/long_mult_test -username someone_else
# Assuming the dump file existed. Load the dumped bacct data into 'worker_resource_usage' table:
load_resource_usage.pl -url mysql://username:secret@hostname:port/long_mult_test -source long_mult.bacct
# Provide your own command to fetch and parse the worker_resource_usage data from:
load_resource_usage.pl -url mysql://username:secret@hostname:port/long_mult_test -source "bacct -l -C 2012/01/25/13:33,2012/01/25/14:44 |" -meadow_type LSF
OPTIONS
-help : print this help
-url <url string> : url defining where hive database is located
-username <username> : if it wasn't you who ran the pipeline, the name of that user can be provided
-source <filename> : alternative source of worker_resource_usage data. Can be a filename or a pipe-from command.
-meadow_type <type> : only used when -source is given. Tells which meadow type the source filename relates to. Defaults to the first available meadow (LOCAL being considered as the last available)
LICENSE
Copyright [1999-2015] Wellcome Trust Sanger Institute and the EMBL-European Bioinformatics Institute
Copyright [2016-2021] EMBL-European Bioinformatics Institute
Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License
is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and limitations under the License.
Please subscribe to the Hive mailing list: http://listserver.ebi.ac.uk/mailman/listinfo/ehive-users to discuss Hive-related questions or to be notified of our updates


|
||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object java.lang.Throwable java.lang.Exception org.codehaus.aspectwerkz.annotation.expression.ast.ParseException
public class ParseException
This exception is thrown when parse errors are encountered. You can explicitly create objects of this exception type by calling the method generateParseException in the generated parser.
You can modify this class to customize your error reporting mechanisms so long as you retain the public fields.
| Field Summary | |
|---|---|
Token
|
currentToken
This is the last token that has been consumed successfully. |
protected
String
|
eol
The end of line string for this machine. |
int[][]
|
expectedTokenSequences
Each entry in this array is an array of integers. |
protected boolean
|
specialConstructor
This variable determines which constructor was used to create this object and thereby affects the semantics of the "getMessage" method (see below). |
String
[]
|
tokenImage
This is a reference to the "tokenImage" array of the generated parser within which the parse error occurred. |
| Constructor Summary | |
|---|---|
ParseException
()
The following constructors are for use by you for whatever purpose you can think of. |
|
ParseException
(
String
message)
|
|
ParseException
(
Token
currentTokenVal,
int[][] expectedTokenSequencesVal,
String
[] tokenImageVal)
This constructor is used by the method "generateParseException" in the generated parser. |
| Method Summary | |
|---|---|
protected
String
|
add_escapes
(
String
str)
Used to convert raw characters to their escaped version when these raw version cannot be used as part of an ASCII string literal. |
String
|
getMessage
()
This method has the standard behavior when this object has been created using the standard constructors. |
| Methods inherited from class java.lang. Throwable |
|---|
fillInStackTrace
,
getCause
,
getLocalizedMessage
,
getStackTrace
,
initCause
,
printStackTrace
,
printStackTrace
,
printStackTrace
,
setStackTrace
,
toString
|
| Methods inherited from class java.lang. Object |
|---|
clone
,
equals
,
finalize
,
getClass
,
hashCode
,
notify
,
notifyAll
,
wait
,
wait
,
wait
|
| Field Detail |
|---|
protected boolean specialConstructor
public Token currentToken
public int[][] expectedTokenSequences
public String [] tokenImage
protected String eol
| Constructor Detail |
|---|
public ParseException ( Token currentTokenVal, int[][] expectedTokenSequencesVal, String [] tokenImageVal)
public ParseException ()
public ParseException ( String message)
| Method Detail |
|---|
public String getMessage ()
getMessage
in class
Throwable
protected String add_escapes ( String str)
|
||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |


There are many different ways to classify the ways we act and think. One interesting way to look at how you think is with the Gregorc Thinking Style After taking this test myself, I learned that I am mostly an abstract sequential thinker.
Abstract sequential thinking is mostly defined by someone who:
AS thinkers generally struggle with:
I definitely agree that a lot of these traits have summed up my experiences so far in DBC. I enjoy talking with other people and helping them solve their answers. I have had a fun time working through the ruby problems and addressing problems that poeple are having.
I do feel that I haven't had enough time to work through a lot of the HTML and CSS stuff so I would like to revisit that stuff in the future. Luckily, I have done a bit of Ruby in the past so I do feel comfortable with the amount of time that we have been given to learn it. I do find myself sometimes struggling to fill out the reflections, or even blog, as it isn't necessarily what I find most enjoyable about programming. (though I definitely see the value in it!)


dist = np.sum(np.square(f1-f2))
print(dist)
sim = np.dot(f1, f2.T)
print(sim)
//diff = np.subtract(source_feature, target_feature)
//dist = np.sum(np.square(diff),1)
img = cv2.imread("/Users/aub3/3.jpg")
f3 = model.get_feature(img)
dist1 = np.sum(np.square(f1-f2))
dist2 = np.sum(np.square(f1-f3))
print(dist1,dist2)


Kenneth (Page) Swanson
US Citizen Lives in Germany Email
ka.pageswanson at proton.me GitHub pageswanson
Web pageswanson.github.io/homepage
Professional programmer with experience in production software for a
.NET ecosystem with C#, MS-SQL, and ES5/ES6. As of today: teaching
coding locally, renewing personal interest in C through independent
work, freelancing with JavaScript using a functional approach, and
learning Rust via a sequencer clone project. A native English speaker
learning German (beginner competency).
Experience
Software Developer in Residence / New Haven Free Public Library -
New Haven, CT
05 / 2020 → Present
- Serves as a community reference for learning
programming at the library. Hosting bi-weekly sessions emphasizing core
web technologies as an entry point to coding with 200 participants since
initial series. Holds office hours for help with programming projects
(JavaScript, HTML, CSS)
- Introduced concepts in audio software through
graphical programming, creating instruments for sound synthesis
(PureData)
- Led a database survey series where students
followed tutorials on query building, understanding schema, and finally
building and running a micro database server (SQLite, Deno)
Full-stack Software Engineer / Abrigo (Sageworks) - Remote
09 / 2017 → 11/2021
- Developed applications for large data transfer
alongside a team of 10 engineers, product managers, and QA to enable a
rapid and stable financial import pathway (Agile w/ Jira, Git &
Bitbucket)
- Provided hourly support for client-facing project
managers, responding to service requirements for over 1000 financial
institutions across the US, with extensive assistance during the 2020
national SBA disbursement period for institutions providing loans at the
outset of the COVID-19 pandemic, aiding in the pipeline for subscribers
to service more than 1 million in funds.
- Part of a frontend developer initiative encouraging
resource sharing across teams, build process and workflow improvements
(Vue.js)
- Engineered a data migration frontend for managers
to quickly move configurations, relationships, and financial entities
across accounts, with feedback and severity logs to save time on common
merge operations. Iterated the backend with 2 engineers to handle
arbitrary entities using a factory pattern, resolving foreign key
dependencies in schema with entity maps in code (C#, NHibernate, LINQ,
SQL)
- Scaled a document import service to onboard client
image repositories and associate existing financials. Incorporated
entity layer for import transactions and added unit tests, task logging
with line-item feedback. Included an avenue for internal distribution to
customers for faster advisory feedback. Reduced processing times from 24
hour benchmarks to 2 hour run times with comparable loads (C#, SQL, Moq,
Kibana)
- Engineered a guided walkthrough using component
architectures for a modular onboarding interface. Included automations
for parsing initial extracts to generate mappings, check data integrity,
and poll services to suggest new configurations. Over 70% of newly
serviced clients began using the walkthrough on release, relieving
effort for project managers during setup. Enabled an automated pathway
with greater agency for the financial institution and inspired a series
of similar developer initiatives (AngularJS, components)
Programming Systems TA / Georgia Institute of Technology - Atlanta,
GA
09 / 2016 → 05 / 2017
- Assisted a section of more than 50 student
programmers with algorithm development, data structures, and
concepts in the C language. Held comprehensive review sessions and
weekly office hours (C, MIPS Assembly)
Product & Test Engineering Intern / Texas Instruments - Dallas,
TX
05 / 2016 → 08 / 2016
- Designed an internal web portal to process and
archive data from a test device specification spreadsheet. Built a text
parser to support decision trees and report creation for a team of 5
engineers (Python)
- Created tests with mock requests and included form
sanitization and server-side input type expectations (Promise, Requests,
regex)
Education
Georgia Institute of Technology - Atlanta, GA
05 / 2017
- B.S. Computer Engineering GPA : 3.5 / 4.0
- Selected Coursework Processing of Speech Signals,
Digital Signal Processing, Artificial Intelligence, Computer
Architecture
Projects
04 / 2021 → 06 / 2021
- Collaborated to create a new home for the Enmossed
recording label. From a design draft, developed a page for visitors to
discover and stream recordings produced by the label. The site owner
maintains a static JSON resource consumed by functional components. Used
media queries to create a consistent experience across screens - mobile
or otherwise (ES6, lit-html, Web Components)
TOVA - A Responsive Musical Synthesizer
12 / 2016 → 05 / 2017
- Prototyped a holistic music synthesis device which
responded to audio and notes with a voice selection and melodic phrase.
Contributed an audio feature extraction pipeline based on the chromatic
spectrum for input analysis (Python, librosa, TensorFlow)
Sub 1 Kbps Speech Coder
03 / 2017 → 04 / 2017
- Implemented a 996 bps speech coder which maintained
intelligible speech and speaker fingerprint. Constructed architecture
with elements of LPC, codebook vector quantization and pulse excitation
in MELP (MATLAB)
Guthman-Moog Musical Instrument Competition
2015, 2016, 2017
- 3-time participant, 2-time finalist designing and
building novel synthesizer controllers for the Moog Werkstatt
synthesizer (Arduino)


Deferred promises when this.resolve()
hits the max requests in this.batchSize
List of stringified Primary Keys, even if this.value
is a list of objects, or Resource instances
Is true
when resolve()
is called and first page of results loads up to this.batchSize
objects
Getter -- Same as manager.resources except returns first node
Getter -- get this._resources
but make sure we've actually retrieved the objects first
Throws AttributeError if this.resolve()
hasn't finished
Add a resource to the manager
Resource instance
Calls pending functions in this.deferred
until it's empty. Runs this.resolve()
first if it hasn't been ran yet
DetailOpts
Create a copy of this
except with new value(s)
Get all loaded resources relevant to this relation
Like manager.resources getter except it won't throw an AttributeError and will return with any loaded resources if its ID is listed in this.primaryKeys
Get unique key property from object literal and turn it into a string
Object
Get unique key from resource instance
Resource
Get a single resource from the endpoint given an ID
String | Number
Same as getOne but allow lookup by index
Number
Get the current value and the content type and turn it into a list of primary keys
String
Return a constructor so we can guess the content type. For example, if an object literal
is passed, this function should return Object
, and it's likely one single object literal representing attributes.
If the constructor is an Array
, then all we know is that there are many of these sub items (in which case, we're
taking the first node of that array and using that node to guess). If it's a Number
, then it's likely
that it's just a primary key. If it's a Resource
instance, it should return Resource
. Etc.
Function
Check if values exist on manager
Primary function of the RelatedManager -- get some objects (this.primaryKeys
) related to some
other Resource (this.to
instance). Load the first n objects (this.batchSize
) and set this.resolved = true
.
Subsequent calls may be required to get all objects in this.primaryKeys
because there is an inherent
limit to how many requests that can be made at one time. If you want to remove this limit, set this.batchSize
to Infinity
DetailOpts
Generated using TypeDoc
When sending
this.resolve()
, only send out the firstn
requests wheren
isthis.batchSize
. You can callthis.all()
to recursively get all objects