| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
This allows to share the test for possible relocalisation done in envars.ml.
|
|
|
|
|
|
|
|
|
|
| |
Also standardizing the choice of the default datadir (I don't see why
we should add by default both /usr/local/share/coq and /usr/share/coq
when we know that the installation is in only one of them).
Open question: test for possible relocation of the installed coq
should be done on raw dirname of the executable or on the
standardization of this name wrt symbolic links?
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|\ |
|
|\ \ |
|
|\ \ \ |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
| |_|_|_|_|_|/
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We remove redundant functions `coq_constant`, `gen_reference`, and
`gen_constant`.
This is a first step towards a lazy binding of libraries references.
We have also chosen to untangle `constr` from `Coqlib`, as how to
instantiate the reference (in particular wrt universes) is a
client-side issue. (The client may want to provide an `evar_map` ?)
c.f. #186
|
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
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
|
| | | | | | | |
|
| |/ / / / /
|/| | | | | |
|
|\ \ \ \ \ \ |
|
|/ / / / / /
| | | | | |
| | | | | |
| | | | | | |
We are waiting for an upstream merge of a fix related to coq_makefile2.
|
| | | | | | |
|
| | | | | | |
|
| |_|_|/ /
|/| | | | |
|
| | | |\ \
| | | | | |
| | | | | | |
[checker] [votour] resolve warning 52 fragile constant pattern
|
| | | |/ /
| | | | |
| | | | |
| | | | | |
Also stop using failwith for flow control in tuple_of_string.
|
|\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
resolution trace
|
|\ \ \ \ \ \
| |_|_|_|_|/
|/| | | | | |
|
| | | | | | |
|
| | | | | | |
|
| |_|_|_|/
|/| | | | |
|
| |_|_|/
|/| | | |
|
|\ \ \ \ |
|
|\ \ \ \ \ |
|
|\ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ |
|
|\ \ \ \ \ \ \ \ \ |
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| | | | | | | | | | |
|
| |\ \ \ \ \ \ \ \ \
| |/ / / / / / / / /
|/| | | | | | | | | |
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
The trace only mentions the constant k by which we want to divide
the equation, not anymore the equation we obtain after the division.
Shorter trace, and it won't take much more time to perform the few
Z.div than checking as currently the equality of the initial equation
and the final equation multiplied by k.
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
|
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | |
| | | | | | | | | | |
This fixes bedrock and eliminates warnings.
Thanks Jason Gross for debugging this!
|
|\ \ \ \ \ \ \ \ \ \ |
|