| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
- usage ill-formed for -native-compiler
- compatibility with the configure of 8.4 (-force-caml-version),
though e.g. its force-ocaml-version alias is no longer supported
(but at the same time not documented either, so...)
|
|
are redhibitory.
|
|
|
|
Native_compute is not working properly on Windows due to command line size
limitations and the lack of namespaces in OCaml. Using compiler-libs could
solve this, but it is unclear how to ensure stability w.r.t. future versions of
OCaml.
|
