| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-15 | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject | Maxime Dénès | |
| 2018-02-15 | coq_makefile: Support "" as the prefix in _CoqProject | Joachim Breitner | |
| This fixes #6350 (and even comes with a test case). Refering to other directories as `-R … ""` is maybe not best practice, but some people out there do it, so as long as it does not cause too much trouble, we can continue to support it. | |||
| 2018-02-13 | Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking ↵ | Maxime Dénès | |
| links (#6697) | |||
| 2018-02-09 | [error] Replace msg_error by a proper exception. | Emilio Jesus Gallego Arias | |
| The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now]. | |||
| 2018-02-07 | Possible fix for issue #6697 | Yannick Forster | |
| 2018-01-16 | Merge PR #6466: Replace md5sum/md5 calls by an OCaml program | Maxime Dénès | |
| 2018-01-15 | Avoid shell backticks and improve md5sum.ml error messages | Jacques-Pascal Deplaix | |
| 2018-01-11 | Added newline at the end of usage of coqdep. | Bernhard Schommer | |
| 2018-01-08 | Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts | Maxime Dénès | |
| 2017-12-27 | Add TIMING_SORT_BY and --sort-by to timing scripts | Jason Gross | |
| This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292 | |||
| 2017-12-27 | [API] remove large file containing duplicate interfaces | Enrico Tassi | |
| ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. | |||
| 2017-12-27 | Merge PR #6040: Making coq_makefile usage consistent with what it claims + ↵ | Maxime Dénès | |
| possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments) | |||
| 2017-12-24 | Check the whole string given by md5sum.ml | Jacques-Pascal Deplaix | |
| 2017-12-23 | Replace md5sum/md5 calls by an OCaml program | Jacques-Pascal Deplaix | |
| 2017-12-23 | Registering a printing handler in coq_makefile. | Hugo Herbelin | |
| This allows to fix the non-printing of error messages produced when parsing arguments. | |||
| 2017-12-23 | Forbidding -o and -f in input file of coq_makefile. | Hugo Herbelin | |
| This was apparently either silently doing nothing or failing. | |||
| 2017-12-23 | Removing failure of coq_makefile on no arguments. | Hugo Herbelin | |
| 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. | |||
| 2017-12-18 | Merge PR #6217: Do dependencies in 1 command per file class. | Maxime Dénès | |
| 2017-12-15 | Do dependencies in 1 command per file class. | Gaëtan Gilbert | |
| 2017-12-14 | 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-13 | 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 | |
| `make clean`. | |||
| 2017-12-11 | Fix issue #6387 | Martin Vassor | |
| 2017-12-11 | Restoring 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-07 | Merge PR #6142: Single quotes break on Windows | Maxime Dénès | |
| 2017-11-29 | coq_makefile: pass filenames to coqchk | Ralf Jung | |
| 2017-11-27 | Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate. | Maxime Dénès | |
| 2017-11-24 | Fix coq-makefile ocamldoc call when configured with -annotate. | Gaëtan Gilbert | |
| Fixes #6120. | |||
| 2017-11-22 | Update TimeFileMaker.py to correctly sort timing diffs | Jason Gross | |
| Previously, it was reverse-ordering timing diffs. | |||
| 2017-11-19 | Rename coq-inferior.el -> inferior-coq.el to match provided feature. | Gaëtan Gilbert | |
| Fixes #4988. | |||
| 2017-11-11 | Single quotes break on Windows | Carl 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-01 | Fix 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-12 | Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or ↵ | Maxime Dénès | |
| directory` on every execution | |||
| 2017-10-11 | Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵ | Maxime Dénès | |
| execution | |||
| 2017-10-11 | Merge PR #1143: fix coq_makefile on cygwin | Maxime Dénès | |
| 2017-10-10 | Fix BZ#5780: coq_makefile broken under Cygwin | Ralf 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-06 | TimeFileMaker.py: Allow trailing spaces | Jason Gross | |
| This allows the timing aggregation scripts to handle logs from Travis, which, for some reason, seems to insert trailing spaces. | |||
| 2017-10-05 | Merge 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-05 | Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵ | Maxime Dénès | |
| coq_makefile are in sync (supersed #1039)… | |||
| 2017-10-03 | 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 | |
| proof for coqwc | |||
| 2017-10-03 | Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580). | Maxime Dénès | |
| 2017-09-26 | look for Obligation num or Next Obligation to start proof | Paul Steckler | |
| 2017-09-22 | 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-21 | Properly handle "coq_makefile -Q . Foo" (bug #5580). | Guillaume Melquiond | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |