Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #8015: Output UTF-8 explicitly in timing tools | Jason Gross | 2018-07-08 |
|\ | |||
| * | Output UTF-8 explicitly in timing tools | Jasper Hugunin | 2018-07-07 |
| | | |||
* | | Merge PR #7921: Archive the `gallina` tool | Maxime Dénès | 2018-07-07 |
|\ \ | |/ |/| | |||
* | | Merge PR #7990: Convert timing tool to python3 | Jason Gross | 2018-07-05 |
|\ \ | |||
| * | | Convert timing tools to run with both python2 and python3 | Jasper Hugunin | 2018-07-04 |
| | | | |||
* | | | Fix timing tools on NixOS. | Théo Zimmermann | 2018-07-03 |
|/ / | |||
| * | Archive the `gallina` tool | Vincent Laporte | 2018-06-25 |
|/ | |||
* | Merge PR #7241: [coq_makefile] COQMF_WINDRIVE is empty on linux (fix #7233) | Théo Zimmermann | 2018-06-13 |
|\ | |||
* | | Fix PHONY typo in coq_makefile | Gaëtan Gilbert | 2018-04-27 |
| | | |||
| * | [coq_makefile] COQMF_WINDRIVE is empty on linux (fix #7233) | Enrico Tassi | 2018-04-13 |
|/ | |||
* | docs | Ralf Jung | 2018-03-21 |
| | |||
* | coq_makefile: provide variables to override for adding extra flags | Ralf Jung | 2018-03-20 |
| | |||
* | coq_makefile: FLAG make variables should not contain LIBS | Ralf Jung | 2018-03-20 |
| | |||
* | Closes #6830: coqdep reads options and files from _CoqProject. | Gaëtan Gilbert | 2018-03-06 |
| | | | | Note that we don't look inside -arg for eg -coqlib. | ||
* | Fix #6830: coqdep VDFILE uses too many arguments for fiat-crypto/OSX | Gaëtan Gilbert | 2018-02-28 |
| | | | | | | | | | | | | | | | | We fix as suggested by @JasonGross by reading file names from the _CoqProject when coq_makefile was invoked with one. I made coqdep only look at the .v files from _CoqProject because it's easier this way. Since we're going through the _CoqProject parser we could have coqdep understand more of it but let's leave that to another PR (and maybe someone else). Some projects pass vfiles on the command line, we keep the list of these files to pass them to coqdep via command line even when there is a _CoqProject. Multiple project files is probably broken. | ||
* | Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵ | Maxime Dénès | 2018-02-19 |
|\ | | | | | | | camlp4 | ||
| * | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | Jim Fehrle | 2018-02-17 |
| | | | | | | | | longer use camlp4. | ||
* | | Merge PR #1073: new quick2vo target: like vio2vo, but smarter | Maxime Dénès | 2018-02-15 |
|\ \ | |||
| * | | new quick2vo target: like vio2vo, but smarter | Ralf Jung | 2018-02-15 |
| |/ | |||
* / | Possible fix for issue #6697 | Yannick Forster | 2018-02-07 |
|/ | |||
* | Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts | Maxime Dénès | 2018-01-08 |
|\ | |||
| * | Add TIMING_SORT_BY and --sort-by to timing scripts | Jason Gross | 2017-12-27 |
| | | | | | | | | | | This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292 | ||
* | | [API] remove large file containing duplicate interfaces | Enrico Tassi | 2017-12-27 |
|/ | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client. | ||
* | Merge PR #6217: Do dependencies in 1 command per file class. | Maxime Dénès | 2017-12-18 |
|\ | |||
| * | Do dependencies in 1 command per file class. | Gaëtan Gilbert | 2017-12-15 |
| | | |||
* | | 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 #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. | ||
| | * | | [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 |
| |_|/ |/| | | |||
* | | | Fix coq-makefile ocamldoc call when configured with -annotate. | Gaëtan Gilbert | 2017-11-24 |
| |/ |/| | | | | | Fixes #6120. | ||
| * | 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 5776 - `make` gives `ocamlfind: No such file or directory` on every ↵ | Maxime Dénès | 2017-10-11 |
| | | | | execution | ||
* | 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)… | ||
* | | 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). | ||
* | | Merge PR #990: Prevent warning about DSTROOT being undefined. | Maxime Dénès | 2017-09-15 |
|\ \ | |/ |/| | |||
* | | coq_makefile: fix .merlin generation (FLG -thread) | Enrico Tassi | 2017-08-29 |
| | | |||
* | | coq_makefile: improve documentation | Enrico Tassi | 2017-08-29 |
| | | |||
* | | coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs | Enrico Tassi | 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. | ||
| * | Prevent warning about DSTROOT being undefined. | Guillaume Melquiond | 2017-08-22 |
|/ | |||
* | Merge PR #964: More portable location for the time command. | Maxime Dénès | 2017-08-16 |
|\ | |||
* | | 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. |