| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
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.
|
| | | |
|
| | |
| |
| |
| |
| | |
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.
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | |
| |
| |
| | |
in error messages
|
| | | |
|
| |\| |
|
| | | |
|
| |\| |
|
| | |\ |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This file was only used during ocamldebug sessions (in the dev/db
script). It was containing a large subset of the core cma files,
up to the printing functions. There were a few notable exceptions,
for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
But printers.cma was troublesome to maintain : almost each time an ML file
was added/removed/renamed in the core of Coq, dev/printers.mllib
had to be edited, in addition to the directory-specific .mllib
(kernel/kernel.mllib and co). So I propose here to kill this file,
and put instead in dev/db several "load_printer" of the core cma files.
For that to work, we need to compile kernel/kernel.cma with the right
-dllib and -dllpath options, but that shouldn't hurt (on the contrary).
We also source now the camlpX cma in dev/db, via a new generated file
dev/camlp4.dbg containing a load_printer of either gramlib.cma or
camp4lib.cma.
If one doesn't want to perform the whole "source db" at the start
of an ocamldebug session, then the former "load_printer printers.cma"
could be replaced by:
source core.dbg
load_printer top_printers.cmo
See for instance the minimal dev/base_db.
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
This fixes bug #4828 (https://coq.inria.fr/bugs/show_bug.cgi?id=4828).
|
| |/ /
| |
| |
| |
| | |
It is already very old (shipped with Debian oldstable) and adds file name
support in locations.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Renouncing to bypass the library path given by "camlp5o -where" what
we assume to be the default library location, considering that
-usecamlp5dir is here to deal with the non-standard installation
layout.
Renouncing to find camlp5 libraries in a subdirectory of the ocaml
library directory since we now know that camlp5o is found and that we
have a priori to trust option -where of camlp5o.
Additionally falling back on looking for camlp4 if a camlp5 library is
found but no camlp5 binary. Also using camlp5o as a reference since
after all this is camlp5o that we need.
In particular, this fixes situations where -usecamlp5dir is given but
"camlp5o -where" contradicts it.
If something has to be checked on windows, please tell.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
It has been accidentaly broken since early 2014 (and especially
in 8.5), no easy repair, I won't devote any more hours to this stuff.
Moreover no one seems to care apart from Emilio, but he's ok to work
on this in a separate repository or branch.
I left a dev/doc/ocamlbuild.txt file with a few words about this
experiment.
|
| | |
| |
| |
| | |
Follow-up on Hugo's 1412f9f9.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This patch also disables the -makecmd option and the corresponding test,
since the value is not stored for future use. This prevents gratuitously
failing to configure on FreeBSD.
|
| |\| |
|
| | | |
|
| |\| |
|
Gaetan Gilbert
Emilio Jesus Gallego Arias
Maxime Dénès
Pierre-Marie Pédrot
Guillaume Melquiond
Hugo Herbelin
Théo Zimmermann
Yves Bertot
Matej Kosik
Pierre Letouzey
Jason Gross
Enrico Tassi