aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Remove unused Makefiles in dev/tools/Gravatar Gaëtan Gilbert2017-08-01
| | | | They seem unused since 8f4b7f1 (2007).
* Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Gravatar Maxime Dénès2017-08-01
|\
* \ Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
* \ \ Merge PR #746: Timing on ci via coq_makefile for various projectsGravatar Maxime Dénès2017-07-31
|\ \ \
* \ \ \ Merge PR #923: [api] Fix base_include LTAC parts.Gravatar Maxime Dénès2017-07-28
|\ \ \ \
* \ \ \ \ Merge PR #782: Update API for fiatGravatar Maxime Dénès2017-07-28
|\ \ \ \ \
* \ \ \ \ \ Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceGravatar Maxime Dénès2017-07-28
|\ \ \ \ \ \
| | | | | | * [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | Minor clean up, no sense in having these as they do nothing.
| | | * | | [api] Fix base_include LTAC parts.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |_|/ / / |/| | | |
| | | | * deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | | |
* | | | | Merge PR #886: Fixing what was presumably a typo in the naming conventions fileGravatar Maxime Dénès2017-07-26
|\ \ \ \ \ | |_|_|_|/ |/| | | |
* | | | | [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
| | | | * Alternate way of doing timing on ciGravatar Jason Gross2017-07-21
| | | | | | | | | | | | | | | | | | | | This puts the boilerplate all in one place
| | | | * Separate make from python script for HoTTGravatar Jason Gross2017-07-21
| | | | | | | | | | | | | | | | | | | | HoTT still needs to use the submodule, but this will allow us to more easily see where the build fails, if it does
| | | | * Display timing data travis for various projectsGravatar Jason Gross2017-07-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | HoTT, which builds it's own makefile, and supports timing data, makes use of its own timing script. Everything else goes through the coq-bundled timing scripts.
* | | | | Add AppVeyor infrastructure, launching the test suite under Windows.Gravatar Maxime Dénès2017-07-20
| |_|_|/ |/| | |
* | | | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Maxime Dénès2017-07-19
|\ \ \ \
* | | | | [ci] VST is now built with IGNORECOQVERSION=true.Gravatar Théo Zimmermann2017-07-18
| | | | |
| * | | | [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
|/ / / /
* | | | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layersGravatar Maxime Dénès2017-07-17
|\ \ \ \
* \ \ \ \ Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body ↵Gravatar Maxime Dénès2017-07-17
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | moved to Global).
* \ \ \ \ \ Merge PR #879: Adding debug printers related to universesGravatar Maxime Dénès2017-07-17
|\ \ \ \ \ \
| | | | * | | Fixing what was presumably a typo in the naming conventions file.Gravatar Hugo Herbelin2017-07-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Indeed, "forall x, op x x = x" in not in the list, while this is one of the two standard meanings of idempotence. So, knowing that x, y, ... and not n are used elsewhere for variables names, and elt for constants. Moreover, it is probable that before using consistently x, y and z, I had also used m and n, sometimes. So, a convergent probability that it is (just) a typo.
| | * | | | | Adapting to 91df40272 (body_of_constant_body moved to global).Gravatar Hugo Herbelin2017-07-16
| | | |/ / / | | |/| | |
| * / | | | Adding debug printers related to universes in the default debugger source file.Gravatar Pierre-Marie Pédrot2017-07-14
| |/ / / /
| | * | | Fix a typo in dev/changes.Gravatar Pierre-Marie Pédrot2017-07-14
| | | | |
| | * | | Document the changes in API brought by this series of patches.Gravatar Pierre-Marie Pédrot2017-07-14
| |/ / /
* / / / Adding econstr printer to "include" file.Gravatar Hugo Herbelin2017-07-12
|/ / /
* | | Merge PR #858: [travis] Remove CompCert version check hack.Gravatar Maxime Dénès2017-07-11
|\ \ \
| * | | [travis] Remove CompCert version check hack.Gravatar Emilio Jesus Gallego Arias2017-07-05
| | | | | | | | | | | | | | | | | | | | We now pass `-ignore-coq-version` to CompCert's configure (cf AbsInt/CompCert#188) , thanks to @xavierleroy .
| | * | Makefile: fails if some .vo or .cm* file has no sourceGravatar Pierre Letouzey2017-07-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help preventing weird compilation failures due to leftover object files after deleting or moving some source files By the way: - use plain $(filter-out ...) instead of a 'diff' macro (thanks Jason for the suggestion) - rename FIND_VCS_CLAUSE into FIND_SKIP_DIRS since it contains more than version control stuff nowadays
* | | | Revert fiat-crypto overlayGravatar Jason Gross2017-07-04
|/ / / | | | | | | | | | | | | Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6.
* | | 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
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 04:40:34 +0000