aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
Commit message (Collapse)AuthorAge
* 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
|\ \ \
* \ \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \ \
| * | | | coq_makefile: use -include rather than includeGravatar Enrico Tassi2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | This fixes bedrock and eliminates warnings. Thanks Jason Gross for debugging this!
| * | | | add the only targetGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes the following work correctly: make only TGTS="foo bar" -j2 note that make foo bar -j2 is not doing what you think
| * | | | coq_makefile: avoid spurious ./ in generated .conf fileGravatar Enrico Tassi2017-05-23
| | | | |
| * | | | Restore 8.5, 8.6 compatibility of STDTIME, TIMECMDGravatar Jason Gross2017-05-23
| | | | |
| * | | | coq_makefile: don't quote extra arguments (-arg)Gravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | Restores compatibility with 8.6
| * | | | Make install a single colon target for retro compatibilityGravatar Enrico Tassi2017-05-23
| | | | |
| * | | | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
| | | | |
| * | | | coqdep: remove optimization making makefiles harder to writeGravatar Enrico Tassi2017-05-23
| | | | |
| * | | | coqdep: set FOR_PACK variable for files that need to be packedGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This enables one to have just one rule to compile .ml -> .cmx. By using $(FOR_PACK) in such rule one passes to ocamlopt -for-pack ModName only when necessary. Before this coq_makefile had to generate 2 different rules, depending if the module was mentioned in an .mlpack.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 00:16:22 +0000