Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | Merge PR #6040: Making coq_makefile usage consistent with what it claims + ↵ | 2017-12-27 | ||
|\ \ | | | | | | | | | | possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments) | |||
| | * | Check the whole string given by md5sum.ml | 2017-12-24 | ||
| | | | ||||
| | * | Replace md5sum/md5 calls by an OCaml program | 2017-12-23 | ||
| |/ |/| | ||||
| * | Registering a printing handler in coq_makefile. | 2017-12-23 | ||
| | | | | | | | | | | This allows to fix the non-printing of error messages produced when parsing arguments. | |||
| * | Forbidding -o and -f in input file of coq_makefile. | 2017-12-23 | ||
| | | | | | | | | This was apparently either silently doing nothing or failing. | |||
| * | Removing failure of coq_makefile on no arguments. | 2017-12-23 | ||
| | | | | | | | | | | | | | | | | Nevertheless making option -o of coq_makefile recommended as discussed in PR#6040. This is one way to resolve the inconsistency with the usage which says that all arguments are optional. | |||
* | | Merge PR #6217: Do dependencies in 1 command per file class. | 2017-12-18 | ||
|\ \ | ||||
| * | | Do dependencies in 1 command per file class. | 2017-12-15 | ||
| | | | ||||
* | | | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | 2017-12-14 | ||
|\ \ \ | ||||
* \ \ \ | Merge PR #6388: Fix issue #6387 | 2017-12-14 | ||
|\ \ \ \ | ||||
* \ \ \ \ | Merge PR #1108: [stm] Reorganize flags | 2017-12-13 | ||
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR #6175: Restoring filtering of native files passed to `rm` during ↵ | 2017-12-13 | ||
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | `make clean`. | |||
| | | * | | | | Fix issue #6387 | 2017-12-11 | ||
| |_|/ / / / |/| | | | | | ||||
| * | | | | | Restoring filtering of native files passed to `rm` during `make clean`. | 2017-12-11 | ||
| | |_|_|/ | |/| | | | | | | | | | | | | | Was lost during the coq_makefile 1 -> 2 translation. | |||
| | * | | | [flags] [stm] Reorganize flags. | 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. | 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 | 2017-12-07 | ||
|\ \ \ | ||||
* | | | | coq_makefile: pass filenames to coqchk | 2017-11-29 | ||
| |_|/ |/| | | ||||
* | | | Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate. | 2017-11-27 | ||
|\ \ \ | ||||
| * | | | Fix coq-makefile ocamldoc call when configured with -annotate. | 2017-11-24 | ||
| | | | | | | | | | | | | | | | | Fixes #6120. | |||
* | | | | Update TimeFileMaker.py to correctly sort timing diffs | 2017-11-22 | ||
|/ / / | | | | | | | | | | Previously, it was reverse-ordering timing diffs. | |||
* | / | Rename coq-inferior.el -> inferior-coq.el to match provided feature. | 2017-11-19 | ||
| |/ |/| | | | | | Fixes #4988. | |||
| * | Single quotes break on Windows | 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. | 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 ↵ | 2017-10-12 | ||
|\ | | | | | | | directory` on every execution | |||
| * | Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵ | 2017-10-11 | ||
| | | | | | | | | execution | |||
* | | Merge PR #1143: fix coq_makefile on cygwin | 2017-10-11 | ||
|\ \ | ||||
| * | | Fix BZ#5780: coq_makefile broken under Cygwin | 2017-10-10 | ||
| |/ | ||||
* / | [configure] Support for flambda flags. | 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 | 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 ↵ | 2017-10-05 | ||
|\ | | | | | | | to escape non-UTF-8 file names) | |||
* \ | Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵ | 2017-10-05 | ||
|\ \ | | | | | | | | | | coq_makefile are in sync (supersed #1039)… | |||
| * | | fix compilation on OCaml < 4.04 | 2017-10-03 | ||
| | | | ||||
* | | | Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵ | 2017-10-03 | ||
|\ \ \ | | | | | | | | | | | | | proof for coqwc | |||
* \ \ \ | Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580). | 2017-10-03 | ||
|\ \ \ \ | ||||
| | * | | | look for Obligation num or Next Obligation to start proof | 2017-09-26 | ||
| |/ / / |/| | | | ||||
* | | | | Merge PR #1055: Remove STM vernaculars | 2017-09-22 | ||
|\ \ \ \ | ||||
* \ \ \ \ | Merge PR #1070: Remove remaining occurrences of -just-parsing. | 2017-09-22 | ||
|\ \ \ \ \ | ||||
| | | * | | | Properly handle "coq_makefile -Q . Foo" (bug #5580). | 2017-09-21 | ||
| | | | | | | ||||
| * | | | | | Remove remaining occurrences of -just-parsing. | 2017-09-21 | ||
| | |/ / / | |/| | | | ||||
* / | | | | coq_makefile: dont show errors from failed (ignored) rmdir | 2017-09-20 | ||
|/ / / / | ||||
| | * | | coq_makefile: make sure compile flags for Coq and coq_makefile are in sync | 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. | 2017-09-19 | ||
|/ / / | ||||
* | | | Merge PR #990: Prevent warning about DSTROOT being undefined. | 2017-09-15 | ||
|\ \ \ | |/ / |/| | | ||||
| | * | Supporting library names in utf8 in coqdep. | 2017-09-13 | ||
| |/ |/| | ||||
* | | Merge PR #997: coqdoc: Support comments in verbatim output | 2017-09-07 | ||
|\ \ | ||||
* \ \ | Merge PR #958: coq_makefile: build/use .cma for packed plugins too | 2017-08-31 | ||
|\ \ \ | ||||
| * | | | coq_makefile: fix .merlin generation (FLG -thread) | 2017-08-29 | ||
| | | | | ||||
| * | | | coq_makefile: improve documentation | 2017-08-29 | ||
| | | | | ||||
| * | | | coq_makefile: print error message when coqlib is not set properly | 2017-08-29 | ||
| | | | |