Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | Maxime Dénès | 2017-12-14 |
|\ | |||
* \ | Merge PR #6388: Fix issue #6387 | Maxime Dénès | 2017-12-14 |
|\ \ | |||
* \ \ | Merge PR #1108: [stm] Reorganize flags | Maxime Dénès | 2017-12-13 |
|\ \ \ | |||
* \ \ \ | Merge PR #6175: Restoring filtering of native files passed to `rm` during ↵ | Maxime Dénès | 2017-12-13 |
|\ \ \ \ | | | | | | | | | | | | | | | | `make clean`. | ||
| | | * | | Fix issue #6387 | Martin Vassor | 2017-12-11 |
| |_|/ / |/| | | | |||
| * | | | Restoring filtering of native files passed to `rm` during `make clean`. | Maxime Dénès | 2017-12-11 |
| | | | | | | | | | | | | | | | | Was lost during the coq_makefile 1 -> 2 translation. | ||
| | * | | [flags] [stm] Reorganize flags. | Emilio Jesus Gallego Arias | 2017-12-11 |
| |/ / |/| | | | | | | | | | | | | | | | | | | | | 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. | ||
| | * | [build] Remove coqmktop in favor of ocamlfind. | Emilio Jesus Gallego Arias | 2017-12-10 |
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||
* | | Merge PR #6142: Single quotes break on Windows | Maxime Dénès | 2017-12-07 |
|\ \ | |||
* | | | coq_makefile: pass filenames to coqchk | Ralf Jung | 2017-11-29 |
| | | | |||
* | | | Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate. | Maxime Dénès | 2017-11-27 |
|\ \ \ | |||
| * | | | Fix coq-makefile ocamldoc call when configured with -annotate. | Gaëtan Gilbert | 2017-11-24 |
| | | | | | | | | | | | | | | | | Fixes #6120. | ||
* | | | | Update TimeFileMaker.py to correctly sort timing diffs | Jason Gross | 2017-11-22 |
|/ / / | | | | | | | | | | Previously, it was reverse-ordering timing diffs. | ||
* | / | Rename coq-inferior.el -> inferior-coq.el to match provided feature. | Gaëtan Gilbert | 2017-11-19 |
| |/ |/| | | | | | Fixes #4988. | ||
| * | Single quotes break on Windows | Carl Patenaude Poulin | 2017-11-11 |
|/ | | | | | | | 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. | ||
* | Fix FIXME: use OCaml 4.02 generative functors when available. | Gaëtan Gilbert | 2017-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 ↵ | 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 \. |