aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
* coq_makefile: pass filenames to coqchkGravatar Ralf Jung2017-11-29
|
* Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.Gravatar Maxime Dénès2017-11-27
|\
| * Fix coq-makefile ocamldoc call when configured with -annotate.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | Fixes #6120.
* | Update TimeFileMaker.py to correctly sort timing diffsGravatar Jason Gross2017-11-22
|/ | | | Previously, it was reverse-ordering timing diffs.
* Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gravatar Gaëtan Gilbert2017-11-19
| | | | Fixes #4988.
* Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
| | | | 4.02.3 has been the minimal OCaml version for a while now.
* Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵Gravatar Maxime Dénès2017-10-12
|\ | | | | | | directory` on every execution
| * Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵Gravatar Maxime Dénès2017-10-11
| | | | | | | | execution
* | Merge PR #1143: fix coq_makefile on cygwinGravatar Maxime Dénès2017-10-11
|\ \
| * | Fix BZ#5780: coq_makefile broken under CygwinGravatar Ralf Jung2017-10-10
| |/
* / [configure] Support for flambda flags.Gravatar Emilio Jesus Gallego Arias2017-10-10
|/ | | | | | | | | We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
* TimeFileMaker.py: Allow trailing spacesGravatar Jason Gross2017-10-06
| | | | | This allows the timing aggregation scripts to handle logs from Travis, which, for some reason, seems to insert trailing spaces.
* Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Gravatar Maxime Dénès2017-10-05
|\ | | | | | | to escape non-UTF-8 file names)
* \ Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵Gravatar Maxime Dénès2017-10-05
|\ \ | | | | | | | | | coq_makefile are in sync (supersed #1039)…
| * | fix compilation on OCaml < 4.04Gravatar Enrico Tassi2017-10-03
| | |
* | | Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵Gravatar Maxime Dénès2017-10-03
|\ \ \ | | | | | | | | | | | | proof for coqwc
* \ \ \ Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).Gravatar Maxime Dénès2017-10-03
|\ \ \ \
| | * | | look for Obligation num or Next Obligation to start proofGravatar Paul Steckler2017-09-26
| |/ / / |/| | |
* | | | Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \ \ \
* \ \ \ \ Merge PR #1070: Remove remaining occurrences of -just-parsing.Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \
| | | * | | Properly handle "coq_makefile -Q . Foo" (bug #5580).Gravatar Guillaume Melquiond2017-09-21
| | | | | |
| * | | | | Remove remaining occurrences of -just-parsing.Gravatar Guillaume Melquiond2017-09-21
| | |/ / / | |/| | |
* / | | | coq_makefile: dont show errors from failed (ignored) rmdirGravatar Ralf Jung2017-09-20
|/ / / /
| | * | coq_makefile: make sure compile flags for Coq and coq_makefile are in syncGravatar Emilio Jesus Gallego Arias2017-09-19
| | | | | | | | | | | | | | | | | | | | | | | | E.g. -safe-string is set by configure.ml and made available to both make (via config/Makefile) and coq_makefile (via config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
| * | | Add XML protocol support for Wait.Gravatar Maxime Dénès2017-09-19
|/ / /
* | | Merge PR #990: Prevent warning about DSTROOT being undefined.Gravatar Maxime Dénès2017-09-15
|\ \ \ | |/ / |/| |
| | * Supporting library names in utf8 in coqdep.Gravatar Hugo Herbelin2017-09-13
| |/ |/|
* | Merge PR #997: coqdoc: Support comments in verbatim outputGravatar Maxime Dénès2017-09-07
|\ \
* \ \ Merge PR #958: coq_makefile: build/use .cma for packed plugins tooGravatar Maxime Dénès2017-08-31
|\ \ \
| * | | coq_makefile: fix .merlin generation (FLG -thread)Gravatar Enrico Tassi2017-08-29
| | | |
| * | | coq_makefile: improve documentationGravatar Enrico Tassi2017-08-29
| | | |
| * | | coq_makefile: print error message when coqlib is not set properlyGravatar Enrico Tassi2017-08-29
| | | |
| * | | coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxsGravatar Enrico Tassi2017-08-29
| | | |
* | | | Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \ \ \
| | * | | coq_makefile: do not overwrite CAMLFLAGSGravatar Enrico Tassi2017-08-29
| | | | |
| | * | | coq_makefile: use dedicated variable for extra packagesGravatar Enrico Tassi2017-08-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CAMLPKGS is now used to hold extra findlib -packages The previous solution was to use CAMLFLAGS but since 4.05 an invocation of `ocamlopt -pack useless.cmxa foo.cmx -o packedfoo.cmx` fails saying that `useless.cmxa` is not a compilation unit description. CAMLPKGS is used in all `ocamlopt` invocations but for the one performing the packing.
| | * | | coq_makefile: build/use .cma for packed pluginsGravatar Enrico Tassi2017-08-29
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The build chain is always ml -> cmo -> cma ml -> cmx -> cmxa -> cmxs If we are packing, then it becomes ml -> cmo \ ml -> cmo --> cmo -> cma ml -> cmo / ml -> cmxo \ ml -> cmxo --> cmxo -> cmxa -> cmxs ml -> cmxo / The interest of always having a .cma or .cmxa is that such file can carry linking flags, that in findlib terms means which -package was use to build the plugin.
| | * | coqdoc: Support comments in verbatim outputGravatar Tej Chajed2017-08-29
| | | | | | | | | | | | | | | | Fixes BZ#5700
| | | * Prevent warning about DSTROOT being undefined.Gravatar Guillaume Melquiond2017-08-22
| | |/
* | / Fix coqdoc URLs under Windows.Gravatar Théo Zimmermann2017-08-21
| |/ |/| | | | | URLs on Windows are the same as on Unix, they use / not \.
* | Merge PR #964: More portable location for the time command.Gravatar Maxime Dénès2017-08-16
|\ \
* \ \ Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵Gravatar Maxime Dénès2017-08-16
|\ \ \ | | | | | | | | | | | | wrongly tagged as keywords
* | | | fix coq_makefileGravatar Matej Košík2017-08-12
| | | | | | | | | | | | | | | | | | | | Make sure that when plugin writer does not use -bypass-API, API is opened by default.
| | * | More portable location for the time command.Gravatar Théo Zimmermann2017-08-12
| |/ / |/| | | | | | | | On NixOS in particular, /usr/bin/time doesn't exist.
| | * [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| |/ |/| | | | | | | | | | | | | This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
* | Merge PR #921: [make] remove compat5 file.Gravatar Maxime Dénès2017-08-01
|\ \
* \ \ Merge PR #917: Moving --print-version to -print-version for consistency.Gravatar Maxime Dénès2017-08-01
|\ \ \
* | | | [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.
| | * | [make] remove compat5 file.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |/ / |/| | | | | | | | It is empty and not used anymore.
| * | Adding -print-version in addition to -print-version for consistency.Gravatar Hugo Herbelin2017-07-25
|/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 06:33:15 +0000