| Commit message (Collapse) | Author | Age |
|
|
|
|
| |
Julien Narboux confirmed that it was dead code (GeoProof is not to be
confused with GeoCoq).
|
|\ |
|
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
|
|/
|
|
| |
Fixes BZ#5779
|
|
|
|
|
|
| |
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).
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| |
| | |
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).
|
| | |
|
|/ |
|
|\ |
|
| | |
|
| |
| |
| |
| | |
Fix suggested by Hugo.
|
| | |
|
| |\ |
|
|\ \ \ |
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
|/ / /
| | |
| | |
| | | |
Always output a warning on stderr when a deprecated option is used.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/
| |
| |
| |
| | |
The shell script configure was assuming the existence of option
-camldir which was removed in 333d41a9.
|
|\ \
| | |
| | |
| | | |
more uniform
|
| | |
| | |
| | |
| | | |
others.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |
| | |
| | |
| | |
| | | |
This goes towards an approach where a local layout can be seen as an
installed layout.
|
| | |
| | |
| | |
| | |
| | | |
Consequence: docdir is always defined, no more "" in external
preferences for manual and stdlib when using coqide in -local mode.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
"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
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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]
|
|/ / |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
This removes some remaining support for camlp4 in the infrastructure
and documents the change.
|
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| | |
This makes the dll path consistent both in `-local` and non-local Coq install.
|
|\ \ |
|
| | | |
|
|\ \ \
| | |/
| |/| |
|
| | |
| | |
| | |
| | | |
#5307).
|
| |/
|/|
| |
| |
| | |
Addition of debug info can be prevented using -nodebug at configure
time.
|
| | |
|
| |
| |
| |
| |
| |
| | |
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/).
|
| |
| |
| |
| | |
This was not fixed by b9a15a390f yet.
|
| |
| |
| |
| | |
Was decided during the working group on September, 28th.
|