aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
Commit message (Collapse)AuthorAge
* Merge PR #7321: configure: make -annotate fatal, and color error and warningsGravatar Emilio Jesus Gallego Arias2018-04-26
|\
* | [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc...
| * configure: make -annotate fatal, and color error and warningsGravatar Gaëtan Gilbert2018-04-22
|/ | | | | | Warnings are just too hard to see. Also there is no point keeping a noop option except to point people at the replacement, which does not require configure to succeed.
* [Sphinx] Read version number from configureGravatar Maxime Dénès2018-03-13
|
* Integration of a sphinx-based documentation generator.Gravatar Maxime Dénès2018-03-09
| | | | | | | | The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content.
* Configure now fails with -with-doc yes when a doc dependency is missing.Gravatar Maxime Dénès2018-03-09
|
* Merge PR #6817: [configure]: support for profilesGravatar Maxime Dénès2018-03-08
|\
* | Add some missing flushes in configure.Gravatar Maxime Dénès2018-03-06
| | | | | | | | | | Some messages were sometimes not printed because of the missing flushes. We use a generic combinator suggested by Emilio.
| * configure: -warn-error: now takes a bool so that you can also turn it offGravatar Enrico Tassi2018-03-05
| |
| * configure: profiles (sets of flags)Gravatar Enrico Tassi2018-03-05
| |
| * configure: make Prefs a record rather than a module of refsGravatar Enrico Tassi2018-03-05
|/ | | | In this way it is easy to support multiple defaults
* Merge PR #6283: A pre-commit hook to magically fix whitespace issues.Gravatar Maxime Dénès2018-02-21
|\
* | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | longer use camlp4.
| * Auto-create .git/hooks/pre-commit on ./configureGravatar Jason Gross2018-02-08
|/ | | | | | | | | | | The hook created checks to see if dev/tools/pre-commit exists, and, if so, runs it. This way, we don't have to do any fancy logic to update the git pre-commit hook. The configure script never overwrites an existing precommit hook, so users can disable it by creating an empty pre-commit hook. The check for existence is so that if users check out an old version of Coq, attempting to commit won't give an error about non-existent files.
* Merge PR #6576: generate both binary and text annotationsGravatar Maxime Dénès2018-01-22
|\
| * -annotate deprecated. New options: -annot, -bin-annotGravatar Vadim Zaliva2018-01-19
| |
* | Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < ↵Gravatar Maxime Dénès2018-01-17
|\ \ | | | | | | | | | 2.18.3
| * | Update lablgtk check to be more generalGravatar Jason Gross2018-01-16
| | |
| * | Update configure.ml to only warn on lablgtk 2.16.0Gravatar Jason Gross2018-01-16
| |/ | | | | | | | | | | | | | | | | | | | | The Launchpad packages for lablgtk2 are misconfigured to report 2.16.0 even for much newer versions. This makes building Coq on Ubuntu impossible without modifying configure. This commit fixes that problem. See https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 for the upstream bug. This closes #6585
* | Merge PR #6466: Replace md5sum/md5 calls by an OCaml programGravatar Maxime Dénès2018-01-16
|\ \ | |/ |/|
* | Merge PR #6533: Update the lower-bound of the lablgtk dependency.Gravatar Maxime Dénès2018-01-08
|\ \
* \ \ Merge PR #6501: Document use of ocamldebug from the command line in ↵Gravatar Maxime Dénès2018-01-08
|\ \ \ | | | | | | | | | | | | Cygwin/Windows
| | * | Update the lower-bound of the lablgtk dependency.Gravatar Théo Zimmermann2018-01-04
| |/ / |/| | | | | | | | Closes #6509.
| * | Add instructions for debugging from the command line (and in Windows)Gravatar Jim Fehrle2017-12-29
| | | | | | | | | | | | Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
* | | [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| | | | | | | | | | | | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
| | * Replace md5sum/md5 calls by an OCaml programGravatar Jacques-Pascal Deplaix2017-12-23
| |/
* / [lib] Split auxiliary libraries into Coq-specific and general.Gravatar Emilio Jesus Gallego Arias2017-12-23
|/ | | | | | | | | | | | | | | | | | | | | | | | Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM.
* Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Gravatar Maxime Dénès2017-12-14
|\
* \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \
* \ \ Merge PR #6312: [configure] fix detection of `md5sum`Gravatar Maxime Dénès2017-12-11
|\ \ \
| | * | [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-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.
| * | [configure] fix spelling mistakeGravatar Vincent Laporte2017-12-07
| | |
* | | use preference for ocamlfindGravatar Paul Steckler2017-12-05
| | |
| * | [configure] adds a `select_command` functionGravatar Vincent Laporte2017-12-05
| | |
| * | [configure] fix detection of `md5sum`Gravatar Vincent Laporte2017-12-04
| | |
| | * [kernel] Patch allowing to disable VM reduction.Gravatar Emilio Jesus Gallego Arias2017-12-02
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The patch has three parts: - Introduction of a configure flag `-bytecode-compiler (yes|no)` (due to static initialization this is a configure-time option) - Installing the hooks that register the VM with the pretyper and the kernel conditionally on the flag. - Replacing the normalization function in `Redexpr` by compute if the VM is disabled. We also rename `Coq_config.no_native_compiler` to `native_compiler` and `Flags.native_compiler` to `output_native_objects` [see #4607].
* / check for Num lib if OCaml >= 4.06, #6162Gravatar Paul Steckler2017-12-01
|/
* Surrounding a few places printing file names with quotes when a space occurs.Gravatar Hugo Herbelin2017-11-23
|
* Check findlib version in configure (fix #4270).Gravatar Gaëtan Gilbert2017-11-20
|
* Remove branch on caml version >= 3.10 from configure.Gravatar Gaëtan Gilbert2017-11-19
| | | | We require 4.02.3.
* Remove GeoProof support.Gravatar Maxime Dénès2017-10-11
| | | | | Julien Narboux confirmed that it was dead code (GeoProof is not to be confused with GeoCoq).
* Merge PR #540: [configure] Support for flambda flags.Gravatar Maxime Dénès2017-10-10
|\
| * [flambda] [native] Pass `-Oclassic` to the native compiler.Gravatar Emilio Jesus Gallego Arias2017-10-10
| | | | | | | | | | | | This seems a safe choice as of today, but more advanced users would like to tweak it, or we could even refine it by a configure option if desired.
| * [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" ```
* | Include leading zeros in version infoGravatar Tej Chajed2017-10-09
|/ | | | Fixes BZ#5779
* 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).
* Bump MacOS version number and magic numbers.Gravatar Maxime Dénès2017-09-01
|
* Change version string to 8.8+alpha.Gravatar Maxime Dénès2017-09-01
|
* Merge PR #750: Remove deprecated options of ./configure in 8.8Gravatar Maxime Dénès2017-07-26
|\
* | Set version to 8.7+alpha.Gravatar Maxime Dénès2017-07-13
| | | | | | | | | | It is a valid git tag (unlike 8.7~alpha) and will be considered by most tools as < 8.7.0 (unlike 8.7.0+alpha).