aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
Commit message (Collapse)AuthorAge
* Fix micromega.ml to match generated file and enforce match in make.Gravatar Gaëtan Gilbert2017-11-16
| | | | Mismatch probably caused by c5aca4005.
* Merge PR #1054: Restoring test on ident validity while browsing directory ↵Gravatar Maxime Dénès2017-10-11
|\ | | | | | | structure.
| * Restoring test on ident validity while browsing directory structure.Gravatar Hugo Herbelin2017-10-10
| | | | | | | | | | | | | | | | | | | | | | | | | | The test was abandoned at the time of merging subdirectory browsing between coqdep and coqtop, and to limit at the same time the dependency of coqdep in files such as unicode.cmo. But checking ident validity speeds up browsing in arbitrary directory structure and we restore it for this reason. (One could also say that browsing arbitrary directory structures is not intended, but in practice this may happen, as e.g. reported in BZ#5734.)
* | [configure] Support for flambda flags.Gravatar Emilio Jesus Gallego Arias2017-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" ```
* Fix hardcoded boot dependencies after #1041.Gravatar Gaëtan Gilbert2017-10-07
| | | | | | | Specifically since e88dfedd99a84e9e375f3583be6fd1de3de36c72. There seem to have been no actual errors due to this, only ocaml complaining about missing .cmi files.
* Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Gravatar Maxime Dénès2017-10-05
|\ | | | | | | to escape non-UTF-8 file names)
* | coq_makefile: make sure compile flags for Coq and coq_makefile are in syncGravatar Emilio Jesus Gallego Arias2017-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).
| * Supporting library names in utf8 in coqdep.Gravatar Hugo Herbelin2017-09-13
|/
* Merge PR #958: coq_makefile: build/use .cma for packed plugins tooGravatar Maxime Dénès2017-08-31
|\
* \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \
| | * test-suite: depend on byte compilation tooGravatar Enrico Tassi2017-08-29
| |/ |/| | | | | coq-makefile's tests do depend on this
* | More portable location for the time command.Gravatar Théo Zimmermann2017-08-12
| | | | | | | | On NixOS in particular, /usr/bin/time doesn't exist.
| * [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-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.Gravatar Maxime Dénès2017-08-01
|\
* \ Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceGravatar Maxime Dénès2017-07-28
|\ \
| | * [make] remove compat5 file.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |/ |/| | | | | It is empty and not used anymore.
* | make sure that API-leaks cannot be reintroduced by mistakeGravatar Matej Košík2017-07-26
| |
* | Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\ \
* | | [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
| | |
| * | Add timing scriptsGravatar Jason Gross2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds timing scripts from https://github.com/JasonGross/coq-scripts/tree/master/timing into the tools folder, and integrates them into coq_makefile and Coq's makefile. The main added makefile targets are: - the `TIMING` variable - when non-empty, this creates for each built `.v` file a `.v.timing` variable (or `.v.before-timing` or `.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively) - `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of sorted timings at the end, saving it to `time-of-build-pretty.log` - `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file `time-of-build-before.log` or `time-of-build-after.log`, respectively - `print-pretty-timed-diff` - prints a table with the difference between the logs recorded by `make-pretty-timed-before` and `make-pretty-timed-after`, saving the table to `time-of-build-both.log` - `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a table with the differences between two `.v.timing` files, and saves the output to `time-of-build-pretty.log` - `*.v.timing.diff` - this saves the result of `print-pretty-single-time-diff` for each target to the `.v.timing.diff` file - `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's own Makefile) - makes all `*.v.timing.diff` targets N.B. We need to make `make pretty-timed` fail if `make` fails. To do this, we need to get around the fact that pipes swallow exit codes. There are a few solutions in https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make; we choose the temporary file rather than requiring the shell of the makefile to be bash.
| * | Fix TIMED=1 on Mac OSXGravatar Jason Gross2017-07-08
|/ / | | | | | | This closes [bug #5596](https://coq.inria.fr/bugs/show_bug.cgi?id=5596).
| * Makefile: fails if some .vo or .cm* file has no sourceGravatar Pierre Letouzey2017-07-05
| | | | | | | | | | | | | | | | | | | | | | This should help preventing weird compilation failures due to leftover object files after deleting or moving some source files By the way: - use plain $(filter-out ...) instead of a 'diff' macro (thanks Jason for the suggestion) - rename FIND_VCS_CLAUSE into FIND_SKIP_DIRS since it contains more than version control stuff nowadays
* | Better support for make TIMED=1 on WindowsGravatar Jason Gross2017-06-30
|/ | | | This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
* Makefile.build : restore (temporarily?) the anti-cmi-corruption hacksGravatar Pierre Letouzey2017-06-15
| | | | | | | | Due to the recent conversion of many .mli-only files into .ml files (hugely debatable impact of the API introduction), parallel make may fail badly again (always the same race between ocamlc and ocamlopt for .cmi). Still working on a proper fix, but meanwhile let's reintroduce the old hacks against these corruptions.
* Makefile.build : cleanup now that micromega.ml isn't generated + sync check ↵Gravatar Pierre Letouzey2017-06-14
| | | | | | | of this file There is now a warning if the content of micromega.ml isn't what MExtraction.v would produce.
* Merge PR#498: Bignums as a separate opam packageGravatar Maxime Dénès2017-06-14
|\
* | Makefile.build: do *not* build PLUGINSCMO by default (followup of PR #709)Gravatar Pierre Letouzey2017-06-13
| |
| * BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
|/ | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
* Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ↵Gravatar Matej Košík2017-06-12
| | | | generate them later.
* Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\
* | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
| |
* | Merge PR#515: extract "plugins/micromega/micromega.ml{,i}" files from ↵Gravatar Maxime Dénès2017-06-02
|\ \ | | | | | | | | | "plugins/micromega/MExtraction.v"
| | * mention 'make world' without 'byte' in CHANGES + 2 minor suggestionsGravatar Pierre Letouzey2017-06-01
| | |
| * | a solution that works also with make 3.81Gravatar Matej Kosik2017-06-01
| | |
| * | extract "plugins/micromega/micromega.ml{,i}" files from ↵Gravatar Matej Kosik2017-06-01
| | | | | | | | | | | | "plugins/micromega/MExtraction.v"
* | | Makefile.build: test-suite all = run + report, so don't report againGravatar Gaëtan Gilbert2017-05-31
|/ /
| * Makefile: $(BEST) controls which coqtop is used to build .voGravatar Pierre Letouzey2017-05-30
| | | | | | | | | | | | | | This allows to grant a wish by Hugo: to build coqtop.byte and prelude with it, you could do: make -j BEST=byte states
| * Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2017-05-30
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On a machine for which ocamlopt is available, the make world will now perform bytecode compilation only in grammar/ (up to the syntax extension grammar.cma), and then exclusively use ocamlopt. In particular, make world do not build bin/coqtop.byte. A separate rule 'make byte' does it, as well as bytecode plugins and things like dev/printers.cma. 'make install' deals only with the part built by 'make', while a new rule 'make install-byte' installs the part built by 'make byte'. IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any parallel mix of native and byte rules. These are known to crash sometimes, see below. Instead, do rather 'make -j && make -j byte'. Indeed, apart from marginal compilation speed-up for users not interested in byte versions, the main reason for this commit is to discourage any simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli, and in case of parallel build this may happen at the very moment another ocaml(c|opt) is accessing this .cmi. Until now, this issue has been handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in Makefile.build). But these hacks weren't obvious to extend to ocamlopt -pack vs. ocamlopt -pack. coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML Module influences the .v.d dependency file. Possible values are: -dyndep opt : regular situation now, depends only on .cmxs -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a) -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs -dyndep none : interesting for coqtop with statically linked plugins -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d instead of extensions .cm*, so that the choice is made in the rest of the makefile (see a future commit about coq_makefile) NB: two extra mli added to avoid building unecessary .cmo during 'make world', without having to use the ocamldep -native option. NB: we should state somewhere that coqmktop -top won't work unless 'make byte' was done first
* ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mliGravatar Enrico Tassi2017-05-23
| | | | The .mli only acknowledges the current API. I'm not guilty your honor!
* [camlpX] Enrico's changes to camlp4 removal.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | This removes some remaining support for camlp4 in the infrastructure and documents the change.
* [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* [xml] Restore protocol compatibility with 8.6.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | By default, we serialize messages to the "rich printing representation" as it was done in 8.6, this ways clients don't have to adapt unless they specifically request the new format using option `--xml_format=Ppcmds`
* [pp] Remove richpp from fake_ide.Gravatar Emilio Jesus Gallego Arias2017-03-21
|
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent.
* Converting certain "order-only" (Makefile) dependencies to regular dependencies.Gravatar Matej Kosik2016-10-19
| | | | | | | For some reason "grammar/grammar.cma" was declares only an "order-only" dependency for "*.ml" files generated from "*.ml4". I this that this is a problem because when we change "grammar/*.mlp" files, even tough "grammar/grammar.cma" is regenerated, the actual "*.ml" files (defined by "*.ml4" as well as "grammar/grammar.cma") are not regenerated.
* No more dev/printers.cmaGravatar Pierre Letouzey2016-07-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | This file was only used during ocamldebug sessions (in the dev/db script). It was containing a large subset of the core cma files, up to the printing functions. There were a few notable exceptions, for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug. But printers.cma was troublesome to maintain : almost each time an ML file was added/removed/renamed in the core of Coq, dev/printers.mllib had to be edited, in addition to the directory-specific .mllib (kernel/kernel.mllib and co). So I propose here to kill this file, and put instead in dev/db several "load_printer" of the core cma files. For that to work, we need to compile kernel/kernel.cma with the right -dllib and -dllpath options, but that shouldn't hurt (on the contrary). We also source now the camlpX cma in dev/db, via a new generated file dev/camlp4.dbg containing a load_printer of either gramlib.cma or camp4lib.cma. If one doesn't want to perform the whole "source db" at the start of an ocamldebug session, then the former "load_printer printers.cma" could be replaced by: source core.dbg load_printer top_printers.cmo See for instance the minimal dev/base_db.
* Makefile.build: minor simplificationGravatar Pierre Letouzey2016-07-26
|
* Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4Gravatar Pierre Letouzey2016-07-12
| | | | | | | - With the ?= construction, we avoid warnings about undefined variables, while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make' - Some extra documentation and cleanup
* Removing "READABLE_ML4=" from "Makefile.build"Gravatar Matej Kosik2016-07-12
|
* Removing "VERBOSE=" from "Makefile.build"Gravatar Matej Kosik2016-07-11
|