aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* 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.
* Bump year in headers.Gravatar Maxime Dénès2017-06-01
|
* Add parsers-examples target to fiat-parsers ciGravatar Jason Gross2017-05-23
| | | This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build.
* Switch bedrock to mit-plv baseGravatar Jason Gross2017-05-10
|
* Add bmsherman/topology to the ciGravatar Jason Gross2017-05-01
| | | | | This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk.
* Add bedrock targets src and facadeGravatar Jason Gross2017-04-20
|
* Fix EOL characters in xml protocol documentation.Gravatar Maxime Dénès2017-04-14
|
* Merge PR#563: add XML protocol doc for 8.6Gravatar Maxime Dénès2017-04-14
|\
* | [travis] Use the lite target for fiat-crypto.Gravatar Maxime Dénès2017-04-14
| |
| * update XML protocol doc to 8.6Gravatar Paul Steckler2017-04-13
| |
| * add XML protocol doc for 8.5Gravatar Paul Steckler2017-04-13
|/
* [travis] Backport from trunk: VSTGravatar Emilio Jesus Gallego Arias2017-03-24
|
* [travis] [8.6.only] Backport latest changes from trunk.Gravatar Emilio Jesus Gallego Arias2017-03-22
|
* [travis] Move GeoCoq to allow fail.Gravatar Emilio Jesus Gallego Arias2017-03-10
| | | | We need to agree a bit more with upstream.
* [travis] Backport trunk's travis support.Gravatar Emilio Jesus Gallego Arias2017-03-02
|
* Windows build scripts for 8.6 final.Gravatar Maxime Dénès2016-12-08
|
* Fix paths in 32-bit windows build scripts.Gravatar Maxime Dénès2016-12-08
|
* Add bat files for 8.6rc1 build.Gravatar Maxime Dénès2016-12-07
|
* Add bat files for 8.6beta1 build.Gravatar Maxime Dénès2016-12-07
|
* Merge remote-tracking branch 'github/pr/372' into v8.6Gravatar Maxime Dénès2016-12-02
|\ | | | | | | Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes
* \ Merge remote-tracking branch 'github/pr/368' into v8.6Gravatar Maxime Dénès2016-12-02
|\ \ | | | | | | | | | Was PR#368: Add example in dev/doc/changes involving Tacmach.project
* \ \ Merge remote-tracking branch 'github/pr/369' into v8.6Gravatar Maxime Dénès2016-12-02
|\ \ \ | | | | | | | | | | | | | | | | Was PR#369: Make a note about wit_constr and Constrarg in dev/doc/changes
* \ \ \ Merge remote-tracking branch 'github/pr/371' into v8.6Gravatar Maxime Dénès2016-12-02
|\ \ \ \ | | | | | | | | | | | | | | | Was PR#371: Update dev/doc/changes with things about mem_named_context
* | | | | Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| | | | | | | | | | | | | | | | | | | | | | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
| | | | * (v8.6) Update dev/doc/changes.txt with HintsResolveEntry changesGravatar Jason Gross2016-11-21
| |_|_|/ |/| | |
| * | | (v8.6) Update dev/doc/changes with things about mem_named_contextGravatar Jason Gross2016-11-21
|/ / /
| * / (v8.6) Make a note about wit_constr and Constrarg in dev/doc/changesGravatar Jason Gross2016-11-21
|/ /
| * (v8.6) Add example in dev/doc/changes involving Tacmach.projectGravatar Jason Gross2016-11-21
|/
* [doc] Mention XML protocol on changes.Gravatar Emilio Jesus Gallego Arias2016-11-16
| | | | It may be worth it, also added a note about file reorganization.
* Remove README.win until we come up with new instructions.Gravatar Maxime Dénès2016-11-14
| | | | | The recommended way to install Coq under windows is anyway to use the precompiled installer.
* Move OSX script.Gravatar Maxime Dénès2016-11-10
|
* Add Michael Soegtrop's new script to build windows installer.Gravatar Maxime Dénès2016-11-10
|
* Remove old windows build scripts.Gravatar Maxime Dénès2016-11-10
|
* Merge branch 'fixminimization' into v8.6Gravatar Matthieu Sozeau2016-10-21
|\
| * Remove no longer exported debug printerGravatar Matthieu Sozeau2016-10-21
| |
* | [search] Don't build intermediate lists in search.Gravatar Emilio Jesus Gallego Arias2016-10-20
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch converts the `search_*` functions to use an iter-style API. Consequently, the Search Vernac will produce a message for each search result, greatly improving roundtrip time as IDEs can effectively display the results in a streaming way. It also allows different printers to be used. I didn't observe a performance difference (as things seem to be dominated by printing and `Declaremods`). As a minor tweak, we make search with "Output Name Only" more efficient. Motivation: ----------- Currently, the main search API `Search.generic_search` is an effectful, iteration-based function: ```ocaml val generic_search : int option -> display_function -> unit ``` This type is imposed by `Declaremods`, which exposes an effectful, iteration-based API to traverse Coq library objects. The `Search.search_*` functions try to offer a more functional API by returning a list of pretty printing commands. They need to build an internal intermediate list for that purpose. However, this is a waste of time, as the destination of these lists is to be flushed out by the printer right away.
* More on making the lexer more functional (continuing b8ae2de5 andGravatar Hugo Herbelin2016-10-17
| | | | | | | | | | 8a8caba3). - Adding cLexer.current_file to the lexer state, i.e. making it a component of the type "coq_parsable" of lexer state (it was forgotten in b8ae2de5 and 8a8caba3). - Inlining save_translator/restore_translator which have now lost most of their substance.
* Adding debugging printer for Genarg.ArgT.t.Gravatar Hugo Herbelin2016-10-08
|
* A fix to dev/include.Gravatar Hugo Herbelin2016-08-17
|
* Merge PR #237 into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\
* | Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp).Gravatar Hugo Herbelin2016-07-19
| |
* | FIX: "dev/doc/changes.txt"Gravatar Matej Kosik2016-07-05
| |
| * Add a renaming of Tacexpr.TacDynamicGravatar Jason Gross2016-07-04
|/
* Mention recent renaming of files in dev/doc/changes.txt.Gravatar Maxime Dénès2016-07-03
|
* rename toplevel/cerror.ml into explainErr.ml (too close to the new ↵Gravatar Pierre Letouzey2016-07-03
| | | | lib/cErrors.ml)
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
| | | | For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
|
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 15:33:45 +0000