| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
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/).
|
| |
|
|
| |
Was decided during the working group on September, 28th.
|
| |\ |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This was only when compiling with Camlp4 and it was producing an
assertion failure in asmcomp/emitaux.ml at line 226, reported as
OCaml's bug #6243.
Note: The issue of a problematic compilation with 4.01.0 was raised at
last WG.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
lablgtk"
This reverts commit 469cb750c6c1aa46f77b2a89a36f79f29aa97073.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the
fix to trunk instead.
This reverts commits:
490160d25d3caac1d2ea5beebbbebc959b1b3832.
ef8718a7fd3bcd960d954093d8c636525e6cc492.
6f9cc3aca5bb0e5684268a7283796a9272ed5f9d.
901a9b29adf507370732aeafbfea6718c1842f1b.
|
| |\| |
|
| | |
| |
| |
| |
| | |
When not using ocamlfind, we use a grep-based heuristic to check that lablgtk2
is recent enough. This is an extension of an already-used heuristic.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
This makes sense probably on Windows too, to be evaluated, maybe .exe
suffix should be added.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
paths for ocaml* executables in the generated config/Makefile.
Hoping I'm not doing something wrong. E.g., I don't see why it would
not be ok for windows or macosx too, since e.g. camlp5o was already
with a full path.
|
Maxime Dénès
Pierre-Marie Pédrot
Théo Zimmermann
Yves Bertot
Matej Kosik
Guillaume Melquiond
Pierre Letouzey
Jason Gross
Enrico Tassi
Hugo Herbelin