| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
| |
* When both camlp4 and camlp5 are installed, camlp5 is used by default,
except when -usecamlp4 flag is given to ./configure.
* Otherwise, ./configure pick automatically the available camlpX
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15349 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Since MinGW/Msys doesn't provide a cygpath utility, we emulate
it via an ocaml script tools/mingwpath.ml
* Avoid the crazy sed portions for backslash escaping, instead use
a more robust ocaml script tools/escape_string.ml based on
String.escaped
* No more config/Makefile.template + sed on it, but rather a
"cat << EOF > ..." as for config/coq_config.ml
* Normally, support of Cygwin should be preserved, as well as
mingw32 cross-compilation from linux (cf. myocamlbuild.ml)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15332 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15326 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
./configure -typerex .
It causes (non-fatal) errors when compiling files without a .mli (the problem
seems to have something to do with the flag -intf-suffix .cmi).
In practice, most typerex functionalities don't work well because typerex
fails its lookup into files compiled with -rectypes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15302 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15255 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15254 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Clib that does not depend on camlpX and is made to be shared by all coq
tools/scripts/...
- Lib that is Coqtop specific
As a side effect for the build system :
- Coq_config is in Clib and does not appears in makefiles
- only the BEST version of coqc and coqmktop is made
- ocamlbuild build system fails latter but is still broken
(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
available from OCaml 3.11.2 (see bug #2707)
- fixing outdated address for Coq Club
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
I am not really happy of /etc/xdg/coq ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14906 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14848 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
1/ man dir is now prefix/share/man and not prefix/man git diff!
2/ a data dir option for coqide extra data.
3/ typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14557 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
I assume that once Coq is installed in non-local mode and run from its
installed path, sources are no longer available. The coqsrc variable
doesn't make any sense, then, and its intended value can always be
inferred from Sys.executable_name. Moving it to Envars.coqroot.
Make coqlib optional. Currently, it is set to None only in -local mode
or with ocamlbuild. When set to None, -local layout is assumed
(binaries in ./bin, library in .). The behaviour should not be changed
when an explicit coqlib has been given to ./configure.
This commit should make it possible to run a Coq compiled with -local
from anywhere (no hard-coded absolute path embedded in the
executables, intermediary step to bug #2565). It WILL BREAK settings
re-using source trees after installation in non-local mode (are there
actual use cases for that?).
Hard-coded absolute paths still remain:
- in the build system, so the need to re-run ./configure after moving
the source tree is still expected for now;
- in coqrunbyteflags, I think we are limited by ocaml itself;
- docdir.
All absolute paths should be removed, ultimately.
As a side-effect, simplify computing of Envars.coqbin. I don't see any
good reason to keep it as a function.
Disclaimers:
- initialization of Sys.executable_name is not consistent across all
architectures; relying so much on it might trigger bugs. I'm pretty
sure something will explode if one adds arbitrary symlinks on top of
that;
- ocamlbuild stuff not tested.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
apply patch of bug 668. At last...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
We can be easily substitute Gdk.Windowing by a glance of configure work...
This reverts commit 8b6f6b1c4b60e74dccd5d8c49bdd433e19d53bf4.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14208 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14188 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Because of lablgtk issues, accel_maps can't be customized well on MacOS
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
It looks like a variables definition part of a Makefile. Names are from coq makefiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14080 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is implemented as a C external launching the TerminateProcess
of the Win32 API. This should be considered as quite experimental
(cf. the way we handle pid in the comment of ide_win32_stubs.c).
I don't know how to emulate an interrupt (Ctrl-C), for now the two
button "Restart" and "Interrupt" have the same semantics on win32
(kill the subprocess and start at top).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14044 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
You can quit coqide from the dock and reboot/shutdown will ask you if
you want to save your unsavec files.
Asks for a re"configure".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13974 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
With hints from Daniel de Rauglaudre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
if `pkg-config --exists ige-mac-integration`, coqide.opt will be
able to open files by double-clik in finder on Darwin.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13779 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Its effect is the same as in the default case...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13769 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Untested, see https://bugzilla.redhat.com/show_bug.cgi?id=631302
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13559 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
pngtopnm and pnmtops
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13401 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
I don't have access to an x86_64 computer with 10.6
Maybe for 10.6.0/1/2 special cases aren't required
Reverted commit r13083
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13243 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The choice between camlp4/5 is done during configure with flags
-usecamlp5 (default for the moment) vs. -usecamlp4.
Currently, to have a full camlp4 compatibility, you need to change
all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
into "`EOI" in grammar entries. I've a sed script that does that
(actually the converse), but I prefer to re-think it and check a few
things before branching this sed into the build mechanism.
lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
and try to propose a common interface (cf LexerSig / GrammarSig).
A few incompatible quotations have been turned into underlying code
manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
parsable by both camlp4 and 5. See in particular the fate of
<:str_item< declare ... end >>
Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
This forces to use camlp5 > 5.01.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Ocaml 3.10.0 is already three year old...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13015 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
The csdp path computed by the configure script wasn't used at all, but
was forcing presence of csdp at configure time whereas it is not used
at all in the build process. Instead, we replace the configure-time
check with a runtime check for existence of csdp in $PATH.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12903 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12811 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
autodetection via ./configure, automated installation target
"install-im", and no more patching. Plus documentation of the procedure
in the reference manual.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12790 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
As pointed out by Nima Hoda, bash is not installed everywhere... and
we really don't NEED bash anyway.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12701 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
This allows choosing gmake on *BSD (patch from Nima Hoda).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12689 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
in */*/vo.itarget
On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
if you want a partial build, make a specific rule such as theories-light
Beware: these vo.itarget should not contain comments. Even if this is legal
for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
J'ai ajouté une option '-force-caml-version' au ./configure pour
passer outre la vérification de la version de OCaml. La barre a été
mise à 3.09.3 parce que Khepri (Debian Etch = oldstable) continue de
faire tourner le bench en utilisant OCaml 3.09.3.
Pour info, Coq 8.2 compile avec la 3.08.4, mais pas le trunk.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12473 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Ajout d'un test d'existence de pngtopnm et de pnmtops dans le
./configure
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12471 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- Removed unneeded bashisms. (sh and dash are fine with the current build system.)
- Removed workaround for camlp4.opt on BSD.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12362 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In trunk: New strategy for compiling and finding index_url.txt. After
all, this file is not specific to CoqIDE but to the
documentation. Hence, it seems better to install it close to the
documentation. If the documentation is locally installed, it is easy
to find the file index_url.txt but what to do if the documentation is
remote? We would need a http getter. Does this mean we have to rely on
wget or so? In the absence of answer to this question, it seems
reasonable, first to assume the doc to be locally installed, second to
have a local copy of index_url.txt ready in the installation directory
of CoqIDE.
Also added an "automatic" field in the CoqIDE url preference to
prevent the user to have to update his preference file every time a
new version of Coq is out and the link to the doc change.
In 8.2: Added a minima the installation of index_urls.txt but the user
will have to update its preferences because the links
"http://coq.inria.fr/doc/Reference-Manual010.html#..." do not longer
exist.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12278 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12105 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
(r12063) for smooth compilation/installation under Solaris (/bin/sh ->
/bin/bash, -or -> -o in find, echo -n -> printf, ! in test rather than
in if).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12065 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12048 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Import of Coq_config via myocamlbuild_config.ml, instead of my get_env
* As a consequence, we enrich this Coq_config with stuff that was
only in config/Makefile
* replace the big ugly find by some dependencies against source files
* by the way: build csdpcert, with the right aliases.
I've tried to escape things properly for windows in ./configure,
but this isn't fully tested yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12046 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
hypotheses in induction, unbalanced parenthesis in ltac call stack
printer) and 12003 (late update of CREDITS) + update of magic numbers
(using a somehow arbitrary value between the 8.2 magic numbers and the
possibly forthcoming 8.3 magic numbers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12007 85f007b7-540e-0410-9357-904b9bb8a0f7
|