aboutsummaryrefslogtreecommitdiff
path: root/tools
AgeCommit message (Collapse)Author
2017-12-13Merge PR #6175: Restoring filtering of native files passed to `rm` during ↵Maxime Dénès
`make clean`.
2017-12-11Fix issue #6387Martin Vassor
2017-12-11Restoring filtering of native files passed to `rm` during `make clean`.Maxime Dénès
Was lost during the coq_makefile 1 -> 2 translation.
2017-12-11[flags] [stm] Reorganize flags.Emilio Jesus Gallego Arias
We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag.
2017-12-10[build] Remove coqmktop in favor of ocamlfind.Emilio Jesus Gallego Arias
We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
2017-12-07Merge PR #6142: Single quotes break on WindowsMaxime Dénès
2017-11-29coq_makefile: pass filenames to coqchkRalf Jung
2017-11-27Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.Maxime Dénès
2017-11-24Fix coq-makefile ocamldoc call when configured with -annotate.Gaëtan Gilbert
Fixes #6120.
2017-11-22Update TimeFileMaker.py to correctly sort timing diffsJason Gross
Previously, it was reverse-ordering timing diffs.
2017-11-19Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gaëtan Gilbert
Fixes #4988.
2017-11-11Single quotes break on WindowsCarl Patenaude Poulin
As it is, running a `Makefile.coq` on Windows produces the following error: `cut: ': No such file or directory` Changing to double quotes fixes this.
2017-11-01Fix FIXME: use OCaml 4.02 generative functors when available.Gaëtan Gilbert
4.02.3 has been the minimal OCaml version for a while now.
2017-10-12Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵Maxime Dénès
directory` on every execution
2017-10-11Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵Maxime Dénès
execution
2017-10-11Merge PR #1143: fix coq_makefile on cygwinMaxime Dénès
2017-10-10Fix BZ#5780: coq_makefile broken under CygwinRalf Jung
2017-10-10[configure] Support for flambda flags.Emilio Jesus Gallego Arias
We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
2017-10-06TimeFileMaker.py: Allow trailing spacesJason Gross
This allows the timing aggregation scripts to handle logs from Travis, which, for some reason, seems to insert trailing spaces.
2017-10-05Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Maxime Dénès
to escape non-UTF-8 file names)
2017-10-05Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵Maxime Dénès
coq_makefile are in sync (supersed #1039)…
2017-10-03fix compilation on OCaml < 4.04Enrico Tassi
2017-10-03Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵Maxime Dénès
proof for coqwc
2017-10-03Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).Maxime Dénès
2017-09-26look for Obligation num or Next Obligation to start proofPaul Steckler
2017-09-22Merge PR #1055: Remove STM vernacularsMaxime Dénès
2017-09-22Merge PR #1070: Remove remaining occurrences of -just-parsing.Maxime Dénès
2017-09-21Properly handle "coq_makefile -Q . Foo" (bug #5580).Guillaume Melquiond
2017-09-21Remove remaining occurrences of -just-parsing.Guillaume Melquiond
2017-09-20coq_makefile: dont show errors from failed (ignored) rmdirRalf Jung
2017-09-19coq_makefile: make sure compile flags for Coq and coq_makefile are in syncEmilio Jesus Gallego Arias
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).
2017-09-19Add XML protocol support for Wait.Maxime Dénès
2017-09-15Merge PR #990: Prevent warning about DSTROOT being undefined.Maxime Dénès
2017-09-13Supporting library names in utf8 in coqdep.Hugo Herbelin
2017-09-07Merge PR #997: coqdoc: Support comments in verbatim outputMaxime Dénès
2017-08-31Merge PR #958: coq_makefile: build/use .cma for packed plugins tooMaxime Dénès
2017-08-29coq_makefile: fix .merlin generation (FLG -thread)Enrico Tassi
2017-08-29coq_makefile: improve documentationEnrico Tassi
2017-08-29coq_makefile: print error message when coqlib is not set properlyEnrico Tassi
2017-08-29coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxsEnrico Tassi
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29coq_makefile: do not overwrite CAMLFLAGSEnrico Tassi
2017-08-29coq_makefile: use dedicated variable for extra packagesEnrico Tassi
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.
2017-08-29coq_makefile: build/use .cma for packed pluginsEnrico Tassi
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.
2017-08-29coqdoc: Support comments in verbatim outputTej Chajed
Fixes BZ#5700
2017-08-22Prevent warning about DSTROOT being undefined.Guillaume Melquiond
2017-08-21Fix coqdoc URLs under Windows.Théo Zimmermann
URLs on Windows are the same as on Unix, they use / not \.
2017-08-16Merge PR #964: More portable location for the time command.Maxime Dénès
2017-08-16Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵Maxime Dénès
wrongly tagged as keywords
2017-08-12fix coq_makefileMatej Košík
Make sure that when plugin writer does not use -bypass-API, API is opened by default.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:29:22 +0000