| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
making configure option -opt deprecated.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
I didn't understand the purpose of the previous behavior so please check this commit
|
| | |
|
| |
|
|
| |
This makes the hammer tools/mkwinapp.ml kind of obsolete
|
| |
|
|
|
|
| |
CoqIDE seems to work, but for random pauses that make you think
of a thread deadlock, but then, after a few seconds, things make
progress again. This happens only seldom on my virtual machine.
|
| | |
|
| | |
|
| |
|
|
| |
md5sum check remains not portable.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
According to http://caml.inria.fr/mantis/view.php?id=6346, this flag
causes ocamlc to fail on the latest version of xcode, because clang now
errors on -fno-defer-pop. According to the same issue, -fno-defer-pop
is required for computed gotos if you're using gcc 1.xx, but not gcc
3.4.0 nor 4.4.7 (nor presumably other reasonably modern versions of
gcc). I haven't actually tested this, as I don't have a mac, but it's a
relatively small change.
Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Anyway, a few syntactic features of 3.12 were already used here and
there (e.g. local opening via Foo.(...), or the record shortcut
{ field; ... }). Hence compiling with 3.11 wasn't working anymore.
Already take advantage of the following 3.12.1 features :
- "module type of ..." in CArray, CList, CString ...
- "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output
via our coqdep to localize the .ml4 modules :-)
The -ml-synonym option (+ various bugfixes) is the reason for asking
3.12.1 directly and not just 3.12.0. After all, if debian stable is
providing 3.12.1, then everybody has it ;-)
|
| |
|
|
|
|
|
|
|
| |
Problems:
- strip may not be "strip" but "i686-bla-strip", hence we ask ocamlc -config
the value of "ranlinb" and replace ranlib by strip obtaining
"i686-bla-strip" from "i686-bla-ranlib"
- coq_makefile was not quoting the plugins/ paths
- coq_makefile was quoting twice camlpX (the shell of cygwin was confused)
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
NB: Please re-run ./configure after pulling this commit
For launching ocamlc/ocamlopt, coqmktop doesn't use Sys.command anymore,
but rather CUnix.sys_command, which is based on Unix.create_process.
This way, we do not need to bother with the underlying shell
(/bin/sh or cmd.exe) and the way arguments are to be quoted :-).
Btw, many cleanups of coqmktop.
Only difficulty: the -coqrunbyteflags of ./configure is a "meta-option"
that collect as a string several sub-options to be given by coqmktop to ocamlc.
For instance ./configure -coqrunbyteflags "-dllib -lcoqrun". We need now to
parse all these sub-options. To ease that, I've made the following changes
to the ./configure options:
* The -coqrunbyteflags and its blank-separated argument isn't accepted
anymore, and is replaced by a new option -vmbyteflags which expects
a comma-separated argument. For instance:
./configure -vmbyteflags "-dllib,-lcoqrun"
Btw, on this example, the double-quotes aren't mandatory anymore :-)
* The -coqtoolsbyteflags isn't accepted anymore. To the best of my
knowledge, nobody ever used it directly (it was internally triggered
as a byproduct of the -custom option). The only interest I can think of
for this option was to cancel the default use of ocamlc custom-linking
on Win32 and MacOS. For that, ./configure now provides a -no-custom option.
|
| |
|
|
| |
Moreover, cleanup of System.connect (used by the "external" tactic).
|
| | |
|
| |
|
|
| |
config/coq_config.ml
|
| |
|
|
|
|
| |
Also, we need :=, so that it's evaluated immediately, rather than
becoming a self-recursive variable. This fixes the "Undefined variable
'C'" error that make keeps spewing.
|
| | |
|
| |
|
|
| |
md5sum check remains not portable.
|
|
|
configure is now just a minimal wrapper around the new configure.ml.
This configure.ml is runned with the same ocaml used during
compilation, and starts with a #load "unix.cma".
For now, this new configure script is meant to be 99% compatible
with the old one. Known incompatibilities : the --foo option format
(with two --) isn't supported anymore, use -foo options instead.
Let me know if you encounter any other changes.
Internals:
- We use our own "run" command (based on Unix.create_process) to avoid
relying on some specific shell (/bin/sh or cmd.exe).
- We should have far less issues with filename quoting under windows
since we almost never rely on (cygwin) shell anymore. This remains
to be fully tested, though.
- dev/ocamldebug-coq is slightly different now, to ease its generation
|
Maxime Dénès
Guillaume Melquiond
Matthieu Sozeau
Enrico Tassi
Benjamin Gregoire
Hugo Herbelin
Pierre Boutillier
Pierre Boutillier
jbapple
Jason Gross
Pierre Letouzey
Pierre-Marie Pédrot