| Commit message (Collapse) | Author | Age |
... | |
| | | |
|
| | | |
|
| | | |
|
| | | |
|
|\ \ \ |
|
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is necessary in order for clients to identify the results of
queries. This is a minor breaking change of the protocol, affecting
only this particular call.
This change is necessary in order to fix bug ####.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
According to
https://www.gnu.org/software/make/manual/html_node/Options_002fRecursion.html#Options_002fRecursion
it's not necessary, because we pass `-j ${NJOBS}` to the top-level `make`
invocation in `.travis.yml`. Additionally, explicitly passing `-j` in,
e.g., fiat-crypto, results in error messages such as
```
make[2]: *** write jobserver: Bad file descriptor. Stop.
make[2]: *** Waiting for unfinished jobs....
make[2]: *** write jobserver: Bad file descriptor. Stop.
make[1]: *** [coqprime] Error 2
make[1]: INTERNAL: Exiting with 1 jobserver tokens available; should be 2!
make[1]: Leaving directory `/home/travis/build/JasonGross/coq/_build_ci/fiat-c
```
because the `-j` on the `make` in the `ci-fiat-crypto.sh` script
disables jobserver mode, and the submake in fiat-crypto to make coqprime
does not explicitly pass `-j`, and so reenables jobserver mode, and then
`make` gets very confused.
Commit made with
```bash
cd dev/ci
git grep --name-only -- 'make -j ${NJOBS}' | xargs sed s'/make -j \${NJOBS}/make/g' -i
git grep --name-only -- 'make -f Makefile.coq -j ${NJOBS}' | xargs sed s'/make -f Makefile.coq -j \${NJOBS}/make -f Makefile.coq/g' -i
```
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The lite target depends on having the submodule cloned to generate the
list of files to not build.
|
| | | | |
| | | | |
| | | | |
| | | | | |
This will avoid stupid merge conflicts in the future.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Except I have disabled the minimization of universes after sections as
it seems to interfere with the STM machinery causing files like
test-suite/vio/print.v to loop when processed asynchronously.
This is very peculiar and needs more investigation as the aforementioned
file does not have any sections or any universe polymorphic definitions!
commit fc785326080b9451eb4700b16ccd3f7df214e0ed
Author: Amin Timany <amintimany@gmail.com>
Date: Mon Apr 24 17:14:21 2017 +0200
Revert STL to monomorphic
commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996
Author: Amin Timany <amintimany@gmail.com>
Date: Mon Apr 24 17:02:42 2017 +0200
Try unifying universes before apply subtyping
commit ff393742c37b9241c83498e84c2274967a1a58dc
Author: Amin Timany <amintimany@gmail.com>
Date: Sun Apr 23 13:49:04 2017 +0200
Compile more of STL with universe polymorphism
commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6
Author: Amin Timany <amintimany@gmail.com>
Date: Tue Apr 18 21:26:45 2017 +0200
Made more progress on compiling the standard library
commit b8550ffcce0861794116eb3b12b84e1158c2b4f8
Author: Amin Timany <amintimany@gmail.com>
Date: Sun Apr 16 22:55:19 2017 +0200
Make more number theoretic modules monomorphic
commit 29d126d4d4910683f7e6aada2a25209151e41b10
Author: Amin Timany <amintimany@gmail.com>
Date: Fri Apr 14 16:11:48 2017 +0200
WIP more of standard library compiles
Also: Matthieu fixed a bug in rewrite system which was faulty when
introducing new morphisms (Add Morphism) command.
commit 23bc33b843f098acaba4c63c71c68f79c4641f8c
Author: Amin Timany <amintimany@gmail.com>
Date: Fri Apr 14 11:39:21 2017 +0200
WIP: more of the standard library compiles
We have implemented convertibility of constructors up-to mutual
subtyping of their corresponding inductive types. This is similar to
the behavior of template polymorphism.
commit d0abc5c50d593404fb41b98d588c3843382afd4f
Author: Amin Timany <amintimany@gmail.com>
Date: Wed Apr 12 19:02:39 2017 +0200
WIP: trying to get the standard library compile with universe polymorphism
We are trying to prune universes after section ends. Sections add a
load of universes that are not appearing in the body, type or the
constraints.
|
|\ \ \ \ |
|
| | | | | |
|
| |_|_|/
|/| | | |
|
| |/ /
|/| |
| | |
| | |
| | |
| | | |
Bedrock relies on the 8.4 compat flag that we are removing, and we heard
from MIT that they did not plan to port bedrock to more recent versions
of Coq.
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
| |_|_|_|_|/ /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43.
Not necessary anymore since UniMath/UniMath#715 has been merged.
|
|\ \ \ \ \ \ \ |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| | | | | | | | |
|
| |_|/ / / / /
|/| | | | | | |
|
|\ \ \ \ \ \ \
| |_|_|_|/ / /
|/| | | | | | |
|
|\ \ \ \ \ \ \ |
|
| |_|_|_|/ / /
|/| | | | | |
| | | | | | | |
I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed
|
|\ \ \ \ \ \ \ |
|
| | | | | | | | |
|
| | | | | | | | |
|
| |_|_|_|/ / /
|/| | | | | | |
|
| |_|/ / / /
|/| | | | | |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Always output a warning on stderr when a deprecated option is used.
|
| | |_|/ /
| |/| | | |
|
| | | | | |
|
| | | | | |
|
|\ \ \ \ \
| |/ / / /
|/| | | | |
|