aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
Commit message (Collapse)AuthorAge
* 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).
| * Remove deprecated options from ./configureGravatar Théo Zimmermann2017-07-11
| |
* | Set version to 8.7.0~alpha.Gravatar Maxime Dénès2017-07-07
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
| * Bump version number to 8.6.1.Gravatar Maxime Dénès2017-06-26
| |
| * [configure] 'ocaml' is more precise than OCaml as we mean the binary.Gravatar Maxime Dénès2017-06-23
| | | | | | | | Fix suggested by Hugo.
| * ocaml -> OCaml in configure.ml.Gravatar Maxime Dénès2017-06-23
| |
| * Merge PR#729: Fixing an inconsistency between configure and configure.mlGravatar Maxime Dénès2017-06-23
| |\
* | \ Merge PR#749: Normalize deprecation notices of ./configureGravatar Maxime Dénès2017-06-14
|\ \ \
* | | | 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
| * | | Normalize deprecation notices of ./configureGravatar Théo Zimmermann2017-06-11
|/ / / | | | | | | | | | Always output a warning on stderr when a deprecated option is used.
| * | Ensure that warnings new from ocaml > 4.01 remains silent.Gravatar Hugo Herbelin2017-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | Indeed, 8.6 is announced to be compilable with 4.01.0 and it is convenient not seeing warnings about which nothing can be done. Remove deprecation warnings new from ocaml 4.03, as well as warning 52. This is a partial cherry-pick of a77734ad6.
| | * Fixing an inconsistency between configure and configure.ml.Gravatar Hugo Herbelin2017-06-04
| |/ | | | | | | | | The shell script configure was assuming the existence of option -camldir which was removed in 333d41a9.
* | Merge PR#356: Making management of installation directories more structured, ↵Gravatar Maxime Dénès2017-05-30
|\ \ | | | | | | | | | more uniform
| * | Configuration with -local definitively seen as an installation layout like ↵Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | others.
| * | 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.
| * | Configure: viewing compilation in -local itself as an installation layout.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | Consequence: docdir is always defined, no more "" in external preferences for manual and stdlib when using coqide in -local mode.
| * | Configuration: always giving a value to configdir and datadir.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories.
| * | More structure and more code factorization in building defaultGravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | installation paths in unix or win32. There are two layouts (self-contained or unix-like) and we build absolute paths from them. Under unix, there is a fully relative layout (when user gives a prefix) and a standard semi-relative layout (where most file are under /usr/local with the absolute /etc/xdg/coq as an exception). I respected the existing semantics that under cygwin, the unix layout is the default one when prefix is not given, but the self-contained layout is the default one when a prefix is given.
| * | Unifying the layout of installation directories.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | There seems to have been several bugs, when -prefix is given: - Under win32: "" instead of "lib" (presumably introduced in ab442aed8, 2006) - Under win32: datadir, mandir, docdir should presumably be in "share", "man", "doc", as given in default - Under non-win32: coqdoc files should be in latex subdir not emacs subdir
| * | Unified terminology in configure.ml/coq_config.ml: arch_win32 -> arch_is_win32.Gravatar Hugo Herbelin2017-05-29
| | |
| * | Mini-renaming in configure.ml to avoid switching back and forth fromGravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | "libdir" to "COQLIBINSTALL" then "libdir", then "coqlib". For the record, here is how installation options are named at the current time in the different places they are used (if any): Name in Name in Name in Name of option Name in Name of option config/Makefile coqtop -config config/coq_config.ml in configure lib/envars.ml for coqtop/coqdep -------------------------------------------------------------------------------------------------------- COQLIBINSTALL COQLIB coqlib -libdir coqlib -coqlib DOCDIR DOCDIR docdir -docdir docdir CONFIGDIR configdir -configdir DATADIR datadir -datadir BINDIR -bindir MANDIR -mandir EMACSLIB -emacslib COQDOCDIR -coqdocdir Note: in envars.ml, docdir and coqlib are recomputed
* | | 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]
* | | Don't disable deprecation warning for configure.mlGravatar Gaëtan Gilbert2017-05-28
|/ /
* | configure: -local set coqdoc destination dir to ./doc rather than ""Gravatar Enrico Tassi2017-05-23
| |
* | Deprecate -nodoc.Gravatar Théo Zimmermann2017-05-20
| |
* | Enable more warnings, and add -warn-error configure flagGravatar Gaetan Gilbert2017-04-27
| |
* | [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.
* | [safe-string] Enable -safe-string !Gravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | | | | | | | We now build Coq with `-safe-string`, which enforces functional use of the `string` datatype. Coq was pretty safe in these regard so only a few tweaks were needed. - coq_makefile: build plugins with -safe-string too. - `names.ml`: we remove `String.copy` uses, as they are not needed.
* | [META] [build] Install dlls to kernel/byterunGravatar Emilio Jesus Gallego Arias2017-03-10
| | | | | | | | This makes the dll path consistent both in `-local` and non-local Coq install.
* | Merge PR#399: Debug by defaultGravatar Maxime Dénès2017-02-27
|\ \
| * | Deprecate -debug flag.Gravatar Maxime Dénès2017-02-20
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \ \ | | |/ | |/|
| * | Fix configure crash on some version strings of camlp5, e.g. "6.18-exp" (bug ↵Gravatar Guillaume Melquiond2017-01-12
| | | | | | | | | | | | #5307).
| | * Compile with debug information by default.Gravatar Maxime Dénès2017-01-09
| |/ |/| | | | | | | Addition of debug info can be prevented using -nodebug at configure time.
* | OCaml's -dtypes flag is deprecated and replaced by -annot.Gravatar Maxime Dénès2017-01-09
| |
* | Relax required OCaml to 4.02.1.Gravatar Maxime Dénès2017-01-09
| | | | | | | | | | | | We did not decide precisely what minor version we would support, so relaxing. We document why 4.02.0 is not supported (its use is also discouraged by the OCaml team, see e.g. https://ocaml.org/releases/).
| * Fixing another inconsistency when looking for camlp5o when camlp5dir is given.Gravatar Hugo Herbelin2017-01-04
| | | | | | | | This was not fixed by b9a15a390f yet.
* | Bump required OCaml version to 4.02.3.Gravatar Maxime Dénès2016-12-19
| | | | | | | | Was decided during the working group on September, 28th.
| * Set version to 8.6 in configure.Gravatar Maxime Dénès2016-12-08
| |
| * Commit bumping the version number was partial...Gravatar Maxime Dénès2016-12-07
| | | | | | | | | | The sad part of the story is that the script testing this version number is run after tagging by the coq-dev-tools Makefile... will fix that.
| * Set version number to 8.6rc1.Gravatar Maxime Dénès2016-12-07
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Set version number to 8.6beta1.Gravatar Maxime Dénès2016-11-14
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Fix git recognition when in worktrees.Gravatar Théo Zimmermann2016-10-12
| | | | | | | | | | git worktrees have a .git file instead of a .git directory. Using Sys.file_exists is a more general solution which gives true in both cases.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 10:59:54 +0000