aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
* fake_ide: do as coqide to find out coqtop pathGravatar Enrico Tassi2017-07-20
|
* coq-makefile: strip windows drive letter when DESTDIR is not emptyGravatar Enrico Tassi2017-07-20
| | | | | In unix one can concatenate a prefix with an absolute path in order to obtain a valid path. This is not the case on Windows.
* coq-makefile: treat coq_makefile as any other coq binaryGravatar Enrico Tassi2017-07-20
| | | | In particular, find it under $(COQBIN)
* coq-makefile: quote using ' to preserve \ (windows paths)Gravatar Enrico Tassi2017-07-20
|
* In fake_ide, call coqtop.exe instead of coqtop on Win32.Gravatar Maxime Dénès2017-07-20
|
* Avoid using unsupported signals under Windows in fake_ide.Gravatar Maxime Dénès2017-07-20
|
* 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).
* Merge PR #844: Better support for make TIMED=1 on WindowsGravatar Maxime Dénès2017-07-07
|\
* \ Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for WindowsGravatar Maxime Dénès2017-07-05
|\ \
* \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \ \
* | | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | | |
| | * | Fix more potential quoting issues: COQBIN , COQLIBGravatar Jason Gross2017-06-30
| | | |
| | * | Also quote $(COQLIB)/grammarGravatar Jason Gross2017-06-30
| | | | | | | | | | | | In case COQLIB has backslashes, as it does on Windows, or spaces
| | * | Create a variable for CAMLDOC in CoqMakefile.inGravatar Jason Gross2017-06-30
| | | |
| | * | Quote $(OCAMLFIND) in CoqMakefile.in for WindowsGravatar Jason Gross2017-06-30
| |/ / |/| | | | | This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620)
| | * 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)
| * Merge PR#731: Mini-cleaning around OCaml file namesGravatar Maxime Dénès2017-06-27
| |\ | | | | | | | | | | | | This is only a partial merge, we stick with using the standard OCaml (un)capitalize functions.
| | * A cleaning phase about ocaml file names.Gravatar Hugo Herbelin2017-06-27
| | | | | | | | | | | | | | | | | | | | | Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_. We take this constraint into account in tools manipulating Ocaml file names.
* | | Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \ \
* \ \ \ Merge PR#742: Fix `make TIMED=1` garbageGravatar Maxime Dénès2017-06-20
|\ \ \ \
* | | | | [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####.
| * | | | Move TIMER to right in front of COQCGravatar Jason Gross2017-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | Save the COQC variable for the actual path to coqc, as per https://github.com/coq/coq/pull/742#pullrequestreview-44072778
| * | | | Fix `make TIMED=1` garbageGravatar Jason Gross2017-06-15
| | | | | | | | | | | | | | | It should not emit ` (user: 0.00 mem: 2852 ko)` multiple times
| * | | | Strip trailing whitespaceGravatar Jason Gross2017-06-15
|/ / / /
| * / / coqdep: correct support of Local Declare ML ModuleGravatar Pierre Letouzey2017-06-15
|/ / /
* | | Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\ \ \
* | | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Plugin-writers can now use: -bypass-API parameter with "coq_makefile". The effect of that is that instead of -I API the plugin will be compiled with: -I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
* | | | Merge PR#698: Trunk miscGravatar Maxime Dénès2017-06-07
|\ \ \ \
* | | | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* | | | | Fix coq_makefile uninstall target under OSX.Gravatar Maxime Dénès2017-06-01
| | | | |
| | | * | Bump year in headers.Gravatar Maxime Dénès2017-06-01
| | | |/
| * | | removing duplicate line from "tools/CoqMakefile.in"Gravatar Matej Košík2017-05-31
| | | |
| | * | coq_makefile : do not build bytecode versions of plugins by defaultGravatar Pierre Letouzey2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | make install does not install these *.cm(o|a) files either. You could always do manually : - make bytefiles : to build the bytecode *.cm(o|a) files - make install-byte : to install these files - make byte : to compile the whole development with the bytecode version of Coq (this builds the *.cm(o|a) files, but also the .vo via coqc -byte). Technically, the behavior of make is controlled by the OPT variable, which could be -byte or -opt. For instance, 'make byte' corresponds to a 'make OPT:=-byte' Note that coqdep is used with the new option "-dyndep var" : when seeing a Declare ML Module "foo", "coqdep -dyndep var" does not decide whether to depend on foo.cma or foo.cmxs, but rather use some Makefile variables such as foo$(DYNLIB), whose content is later set according to $(OPT)
| | * | 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
* | | | make sure that "ocamllibdep" properly recognizes Ocaml modules that are all ↵Gravatar Matej Košík2017-05-30
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | upper-case At the moment, when one tries to add an Ocaml module to Coq code-base which is composed just from upper-cases letters, the compilation fails with an error: File "......ml", line 1: Error: Error while linking ... Reference to undefined global `FOO' This commit removes the restriction.
* | | Merge PR#356: Making management of installation directories more structured, ↵Gravatar Maxime Dénès2017-05-30
|\ \ \ | | | | | | | | | | | | more uniform
* \ \ \ Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Maxime Dénès2017-05-30
|\ \ \ \ | |_|/ / |/| | |
| | * | Using the same strategy in coqdoc than in coqtop to guess the coqlib.Gravatar Hugo Herbelin2017-05-29
| | | |
| | * | Exporting the suffixes needed to build coqlib, docdir, etc.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to centralize in the configuration file the description of the 3 possible installation layouts (dispatched over directories shared by multiple application as in unix, self-contained style like in windows, local non-installation as with option -local). Also supporting relocalisation when -prefix or -libdir and co is given.
| | * | Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | This goes towards an approach where a local layout can be seen as an installed layout.
* | | | Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\ \ \ \ | |_|/ / |/| | |
| | * | Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc]
* | | | Merge PR#683: coq_makefile: build .cma for each .mlpackGravatar Maxime Dénès2017-05-28
|\ \ \ \
* \ \ \ \ Merge PR#658: [coqdoc] Add keywords in bug 2884.Gravatar Maxime Dénès2017-05-28
|\ \ \ \ \ | |_|_|/ / |/| | | |
| | | * | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
| | * | coq_makefile: build .cma for each .mlpackGravatar Enrico Tassi2017-05-27
| |/ / |/| | | | | | | | | | | | | | | | | | | | It used to generate only .cmo (the packed one). While this works if the plugin has no external dependencies, it does not if it does. The bug affected only bytecode builds
* | | Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 22:12:40 +0000