| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Nothing is done for camlp4
There is an issue with computing camlbindir
|
|
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
|
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
|
|
|
Option -g has no impact on the code generated by GCC, so it is now
systematically added, since it is quite helpful when the VM segfaults
(e.g. bug #4203). Note that, even for a debug build, option -O1 is
preferred to -O0, since -O0 produces assembly code that is much too noisy
for debugging.
For non-debugging builds, -O2 was chosen rather than -O3, since it led to
a noticeably faster VM. I guess even recent GCC compilers still have a
hard time optimizing humongous functions such as the VM.
Here are the results on a simple benchmark: computing the factorial of a
large number with Z and BigZ. (Factorial of 2*6! for Z, of 7! for BigZ.)
For comparison purpose, the timings of native_compute are also provided.
Z BigZ
-O0 6.4 12.3
-O1 4.3 10.7
-O2 2.8 7.3
-O3 3.0 9.3
n_c 2.0 2.4
|
|
|
|
|
|
Long story short: Filname.concat and other OCaml provided functions
to be "cross platform" don't work for us for two reasons:
1. their behavior is fixed when one compiles ocaml, not when one runs it
2. the build system of Coq is unix only
What is wrong with 1 is that if one compiles ocaml for windows
without requiring cygwin.dll (a good thing, since you don't need to
have cygwin to run ocaml) then the runtime always uses \
as dir_sep, no matter if you are running ocaml from a cygwin shell.
If you use \ as a dir separaton in cygwin command lines, without
going trough the cygpath "mangler", then things go wrong.
The second point is that the makefiles we have need a unix like
environment (e.g. we call sed). So you can't compile Coq without
cygwin, unless you use a different build system, that is not what
we support (1 build system is enough work already, IMO).
To sum up: Running coq/ocaml requires no cygwin, comipling coq requires
a unix like shell, hence paths shall be unix like in configure/build stuff.
|
|
|
|
|
|
|
|
|
|
compatibility with pre-1b7d4a033af heuristic in searching camlpX
(continuation of a joint patch with Maxime).
Typo basename -> dirname.
|
|
|
|
Should fix #3396 and #3964.
|
|
Should make the compilation of Coq more robust against LaTeX errors.
See e.g. #4091.
|
|
|
|
|
|
|
