Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵ | Maxime Dénès | 2017-10-12 | |
|\ | | | | | | | directory` on every execution | |||
| * | Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵ | Maxime Dénès | 2017-10-11 | |
| | | | | | | | | execution | |||
* | | Merge PR #1143: fix coq_makefile on cygwin | Maxime Dénès | 2017-10-11 | |
|\ \ | ||||
| * | | Fix BZ#5780: coq_makefile broken under Cygwin | Ralf Jung | 2017-10-10 | |
| |/ | ||||
* / | [configure] Support for flambda flags. | Emilio Jesus Gallego Arias | 2017-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 spaces | Jason Gross | 2017-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 ↵ | Maxime Dénès | 2017-10-05 | |
|\ | | | | | | | to escape non-UTF-8 file names) | |||
* \ | Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵ | Maxime Dénès | 2017-10-05 | |
|\ \ | | | | | | | | | | coq_makefile are in sync (supersed #1039)… | |||
| * | | fix compilation on OCaml < 4.04 | Enrico Tassi | 2017-10-03 | |
| | | | ||||
* | | | Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵ | Maxime Dénès | 2017-10-03 | |
|\ \ \ | | | | | | | | | | | | | proof for coqwc | |||
* \ \ \ | Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580). | Maxime Dénès | 2017-10-03 | |
|\ \ \ \ | ||||
| | * | | | look for Obligation num or Next Obligation to start proof | Paul Steckler | 2017-09-26 | |
| |/ / / |/| | | | ||||
* | | | | Merge PR #1055: Remove STM vernaculars | Maxime Dénès | 2017-09-22 | |
|\ \ \ \ | ||||
* \ \ \ \ | Merge PR #1070: Remove remaining occurrences of -just-parsing. | Maxime Dénès | 2017-09-22 | |
|\ \ \ \ \ | ||||
| | | * | | | Properly handle "coq_makefile -Q . Foo" (bug #5580). | Guillaume Melquiond | 2017-09-21 | |
| | | | | | | ||||
| * | | | | | Remove remaining occurrences of -just-parsing. | Guillaume Melquiond | 2017-09-21 | |
| | |/ / / | |/| | | | ||||
* / | | | | coq_makefile: dont show errors from failed (ignored) rmdir | Ralf Jung | 2017-09-20 | |
|/ / / / | ||||
| | * | | coq_makefile: make sure compile flags for Coq and coq_makefile are in sync | Emilio Jesus Gallego Arias | 2017-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. | Maxime Dénès | 2017-09-19 | |
|/ / / | ||||
* | | | Merge PR #990: Prevent warning about DSTROOT being undefined. | Maxime Dénès | 2017-09-15 | |
|\ \ \ | |/ / |/| | | ||||
| | * | Supporting library names in utf8 in coqdep. | Hugo Herbelin | 2017-09-13 | |
| |/ |/| | ||||
* | | Merge PR #997: coqdoc: Support comments in verbatim output | Maxime Dénès | 2017-09-07 | |
|\ \ | ||||
* \ \ | Merge PR #958: coq_makefile: build/use .cma for packed plugins too | Maxime Dénès | 2017-08-31 | |
|\ \ \ | ||||
| * | | | coq_makefile: fix .merlin generation (FLG -thread) | Enrico Tassi | 2017-08-29 | |
| | | | | ||||
| * | | | coq_makefile: improve documentation | Enrico Tassi | 2017-08-29 | |
| | | | | ||||
| * | | | coq_makefile: print error message when coqlib is not set properly | Enrico Tassi | 2017-08-29 | |
| | | | | ||||
| * | | | coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs | Enrico Tassi | 2017-08-29 | |
| | | | | ||||
* | | | | Merge PR #773: [flags] Remove XML output flag. | Maxime Dénès | 2017-08-29 | |
|\ \ \ \ | ||||
| | * | | | coq_makefile: do not overwrite CAMLFLAGS | Enrico Tassi | 2017-08-29 | |
| | | | | | ||||
| | * | | | coq_makefile: use dedicated variable for extra packages | Enrico Tassi | 2017-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 plugins | Enrico Tassi | 2017-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 output | Tej Chajed | 2017-08-29 | |
| | | | | | | | | | | | | | | | | Fixes BZ#5700 | |||
| | | * | Prevent warning about DSTROOT being undefined. | Guillaume Melquiond | 2017-08-22 | |
| | |/ | ||||
* | / | Fix coqdoc URLs under Windows. | Théo Zimmermann | 2017-08-21 | |
| |/ |/| | | | | | URLs on Windows are the same as on Unix, they use / not \. | |||
* | | Merge PR #964: More portable location for the time command. | Maxime Dénès | 2017-08-16 | |
|\ \ | ||||
* \ \ | Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵ | Maxime Dénès | 2017-08-16 | |
|\ \ \ | | | | | | | | | | | | | wrongly tagged as keywords | |||
* | | | | fix coq_makefile | Matej Košík | 2017-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. | Théo Zimmermann | 2017-08-12 | |
| |/ / |/| | | | | | | | | On NixOS in particular, /usr/bin/time doesn't exist. | |||
| | * | [flags] Remove XML output flag. | Emilio Jesus Gallego Arias | 2017-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. | Maxime Dénès | 2017-08-01 | |
|\ \ | ||||
* \ \ | Merge PR #917: Moving --print-version to -print-version for consistency. | Maxime Dénès | 2017-08-01 | |
|\ \ \ | ||||
* | | | | [toplevel] Remove long ago deprecated and NOOP options. | Emilio Jesus Gallego Arias | 2017-07-27 | |
| | | | | | | | | | | | | | | | | Minor clean up, no sense in having these as they do nothing. | |||
| | * | | [make] remove compat5 file. | Emilio Jesus Gallego Arias | 2017-07-27 | |
| |/ / |/| | | | | | | | | It is empty and not used anymore. | |||
| * | | Adding -print-version in addition to -print-version for consistency. | Hugo Herbelin | 2017-07-25 | |
|/ / | ||||
* | | fake_ide: do as coqide to find out coqtop path | Enrico Tassi | 2017-07-20 | |
| | | ||||
* | | coq-makefile: strip windows drive letter when DESTDIR is not empty | Enrico Tassi | 2017-07-20 | |
| | | | | | | | | | | In unix one can concatenate a prefix with an absolute path in order to obtain a valid path. This is not the case on Windows. | |||
* | | coq-makefile: treat coq_makefile as any other coq binary | Enrico Tassi | 2017-07-20 | |
| | | | | | | | | In particular, find it under $(COQBIN) | |||
* | | coq-makefile: quote using ' to preserve \ (windows paths) | Enrico Tassi | 2017-07-20 | |
| | | ||||
* | | In fake_ide, call coqtop.exe instead of coqtop on Win32. | Maxime Dénès | 2017-07-20 | |
| | | ||||
* | | Avoid using unsupported signals under Windows in fake_ide. | Maxime Dénès | 2017-07-20 | |
| | |