| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
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
|
Enrico Tassi
Pierre Boutillier
Jason Gross
Pierre Letouzey
Pierre-Marie Pédrot