aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
| * Fix libpcre dependency issue under Windows.Gravatar Maxime Dénès2017-06-26
| |
| * Fix proxy setting issueGravatar Michael Soegtrop2017-06-26
| |
| * Fixes bug #5561,#5562 in Windows build systemGravatar Michael Soegtrop2017-06-26
| |
* | Add missing definition and fix #use include;; as suggested by @amintimany.Gravatar Théo Zimmermann2017-06-22
| |
* | Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\ \
* \ \ Merge PR#779: Each user overlay goes into its own file.Gravatar Maxime Dénès2017-06-20
|\ \ \
| | * | [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 ####.
| | | * Remove -j ${NJOBS} from make invocations in the ciGravatar Jason Gross2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 ```
| | | * Fix ci-fiat-crypto to have a proper lite targetGravatar Jason Gross2017-06-16
| | | | | | | | | | | | | | | | | | | | The lite target depends on having the submodule cloned to generate the list of files to not build.
| * | | Each user overlay goes into its own file.Gravatar Théo Zimmermann2017-06-16
| | | | | | | | | | | | | | | | This will avoid stupid merge conflicts in the future.
* | | | Fix a bug in cumulativityGravatar Amin Timany2017-06-16
| | | |
* | | | A short cleanupGravatar Amin Timany2017-06-16
| | | |
* | | | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| | | |
* | | | Squashed commit of the following:Gravatar Amin Timany2017-06-16
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Merge PR#778: Revert "[travis] temporary UniMath overlay"Gravatar Maxime Dénès2017-06-15
|\ \ \
* | | | fix dev/base_include (thanks Zimmi48)Gravatar Pierre Letouzey2017-06-15
| | | |
* | | | Remove bedrock from test suite.Gravatar Maxime Dénès2017-06-15
| |/ / |/| | | | | | | | | | | | | | 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.
* | | Merge PR#749: Normalize deprecation notices of ./configureGravatar Maxime Dénès2017-06-14
|\ \ \
* \ \ \ Merge PR#622: Change the default flag value for Refine.refineGravatar Maxime Dénès2017-06-14
|\ \ \ \
* \ \ \ \ Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \
* | | | | | Temporary overlays because fewer plugins are loaded at startup.Gravatar Maxime Dénès2017-06-14
| | | | | |
* | | | | | [travis] overlay for fiat-crypto (a Require Import FunInd)Gravatar Pierre Letouzey2017-06-14
| | | | | |
* | | | | | [travis] overlays for CompCert and VST (an extra Require Export FunInd)Gravatar Pierre Letouzey2017-06-14
| | | | | |
* | | | | | [travis] fix Software Foundation (one added Require Extraction)Gravatar Pierre Letouzey2017-06-14
| | | | | |
* | | | | | [travis] fix CoLoR by inserting some Require Import FunIndGravatar Pierre Letouzey2017-06-14
| | | | | |
* | | | | | Temporary overlays for bignums.Gravatar Maxime Dénès2017-06-14
| | | | | |
* | | | | | Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#766: Fix ocamldebug for the APIGravatar Maxime Dénès2017-06-13
|\ \ \ \ \ \ \
| | | | | | * | Revert "[travis] temporary UniMath overlay"Gravatar Théo Zimmermann2017-06-13
| |_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43. Not necessary anymore since UniMath/UniMath#715 has been merged.
* | | | | | | Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\ \ \ \ \ \ \
| | | | | * | | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| | | | | | | |
| | | * | | | | [travis] overlay for cornGravatar Pierre Letouzey2017-06-13
| | | | | | | |
| | | * | | | | [travis] extra test ci-bignums (+factorize other scripts)Gravatar Pierre Letouzey2017-06-13
| | | | | | | |
| | | * | | | | [travis] overlay + extra deps for math-classes (and formal-topology)Gravatar Pierre Letouzey2017-06-13
| | | | | | | |
| | | | | * | | Documenting the change of default flag value of Refine.refine.Gravatar Pierre-Marie Pédrot2017-06-13
| | | | | | | |
| | | * | | | | [travis] adapt CoLoR compilation to depend on the bignum packageGravatar Pierre Letouzey2017-06-13
| |_|/ / / / / |/| | | | | |
* | | | | | | Merge PR#764: Point ci-hott at a newer version of HoTTGravatar Maxime Dénès2017-06-13
|\ \ \ \ \ \ \ | |_|_|_|/ / / |/| | | | | |
* | | | | | | Merge PR#715: Add coq-dpdgraph ciGravatar Maxime Dénès2017-06-12
|\ \ \ \ \ \ \
| | | | | * | | [travis overlay] Partially Revert 013c0232953f1f58Gravatar Jason Gross2017-06-12
| |_|_|_|/ / / |/| | | | | | | | | | | | | I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed
* | | | | | | Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\ \ \ \ \ \ \
* | | | | | | | Temporary overlay, waiting for upstream PR merges.Gravatar Maxime Dénès2017-06-12
| | | | | | | |
* | | | | | | | add overlaysGravatar Matej Košík2017-06-12
| | | | | | | |
| | | | | * | | Fix ocamldebug for the APIGravatar Gaëtan Gilbert2017-06-12
| |_|_|_|/ / / |/| | | | | |
| | | * | | | Point ci-hott at a newer version of HoTTGravatar Jason Gross2017-06-11
| |_|/ / / / |/| | | | |
| | | | * | Normalize deprecation notices of ./configureGravatar Théo Zimmermann2017-06-11
| | | | | | | | | | | | | | | | | | | | | | | | Always output a warning on stderr when a deprecated option is used.
| * | | | | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
| | |_|/ / | |/| | |
| | * | | Mirror dpdgraph's travis test more accuratelyGravatar Jason Gross2017-06-08
| | | | |
| | * | | Remove coq-dpdgraph overlayGravatar Jason Gross2017-06-08
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 12:10:41 +0000