| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
See bug #2614.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14519 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
The changes to myocamlbuild.ml didn't compile.
See bug #2614.
Signed-off-by: Tom Prince <tom.prince@ualberta.net>
Signed-off-by: Stephane Glondu <steph@glondu.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14518 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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14457 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We use GenerateConsoleCtrlEvent(CTRL_C_EVENT,...) after having
attached coqide to the console of the coqtop we want to interrupt.
Two caveats:
- This code isn't compatible with Windows < XP SP1.
- It relies on the fact that coqide is now a true GUI app, without
console by default. If for some reason the console of coqide is
restored (for instance via mkwinapp -unset), strange behavior
of the interrupt button is to be expected, at the very least all
instances of coqtop will get Ctrl-C instead of a precise one.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14077 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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is an adaptation of commit 13748 in 8.3 branch
Making coqide console-free can be done via a link flag given to mingw.
In case of problem with this setting, I also include a script mkwinapp.ml
borrowed from project OCaml-Win32 (and slightly modified to allow
restoring the console as well as removing it).
Use:
"mkwinapp coqide.exe" to make it console-free.
"mkwinapp -unset coqide.exe" to go back to usual console app.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14039 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
This is an adaptation of commit 13747 for 8.3 branch
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14038 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13984 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Avoid using Util which depends on Compat and hence Camlp4
- Instead, a small Minilib module specific to coqide, which
duplicate 5 functions from Util (50 lines)
- some dead code removal
- the coqlib variable is asked to coqtop
- remove obsolete Util.check_for_interrupt
This way, coqide only depends on 3 files outside ide/ :
Coq_config, Flags, Ide_intf. Makefile and ocamlbuild are adapted
accordingly.
TODO: how should we signal coqide error, warnings, etc ?
For the moment, some Printf.eprintf, some failwith.
To uniformize later...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13930 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Caveat: in native code, if the executable is a symlink,
Sys.executable_name points to the target of the symlink... this breaks
coqide's way of locating coqtop. Workaround: make bin/coqide.opt a
hardlink (or a copy) instead of a symlink.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13790 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13280 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13064 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
- transition to camlp4, with no compatibility for ocamlbuild+camlp5
(error message)
- fix compilation of decl_mode : a forgotten include, and
Decl_expr which is a pure .mli shouldn't be mentionned in the .mllib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12870 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Remove option -mwindows which isnt working : the GUI binary refuses to
launch in a real windows.
* simplification of ./build. New way of use :
./configure -prefix "" -arch win32 && ./build win32
This way we avoid any tricks with coq_config.ml.
It is also best to avoid ./configure -local otherwise Envars.coqbin ()
will be wrong later.
* Avoid creation of an ad-hoc coq_config in myocamlbuild.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12819 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
we pass -mwindows to the mingw32 linker, this allows coqide.exe to be
considered as a GUI windows program instead of as a console one.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12814 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Details will follow. In a word, we use a gtk+ win32 bundle from gtk.org
to build some (unofficial) mingw32-liblablgtk2 debian packages. Then
./configure -local && ./build win32
is enough to get all native win32 binaries and plugin cmxs from
a confortable linux box.
Next step: an auto-installer :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
Ideally, just install the cross-compiler (mingw32-ocaml on debian)
and launch ./configure -local && ./build win32
For the moment, this needs some twicking of mingw32-ocaml, plus
a mingw32-camlp5 which is not yet distributed. If you want to play with
that, contact me...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12792 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12759 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
|
| |
|
|
|
|
|
|
| |
- no more plugins/interface
- a few missing files in theories.itarget
- a few things required Unix now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12572 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
The camlp4 extension "refutpat" provides a syntax let* for pattern
that are non-exhaustive on purpose (e.g. let* x::l = foo in ...).
A Failure is raised if the pattern doesn't match the expression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12074 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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12041 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Dealing with .vo files was harder than anticipated (issues with
coqdep_boot and the location of the .v files). Current solution
cannot compete for a beauty prize, but well.
Several other issues remain (see top and bottom of myocamlbuild.ml)
- For the moment the coqlib / coqsrc in Coq_config is to be
hacked by hand to add _build/ in it.
- Parallelism is a "no go" for the moment. Ocamlbuild accepts
a -j option, but it has almost no effect experimentally.
(but at least it doesn't take more time than make -j1,
i.e. about 14 min here, instead of about 7 for make -j2)
- After a first full build, ocamlbuild is awfully slow
to detect that nothing has to be redone (1 min 25 here)
To be continued...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12021 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
* a small shell script ./build to drive ocamlbuild
* rules for all the binaries (apart from coqide and coqchk)
* use of ocamlbuild's Echo instead of using shell + sed + awk
for generated files
* Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the
list of things to "clean"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
* generalize the use of .mllib to build all cma, not only in plugins/
* the .mllib in plugins/ now mention Bruno's new _mod.ml files
* lots of .cmo enumerations in Makefile.common are removed, since
they are now in .mllib
* the list of .cmo/.cmi can be retreive via a shell script line,
see for instance rule install-library
* Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
_files_
* a -I option to coqdep_boot allows to control piority of includes
(some files with the same names in kernel and checker ...)
This is quite a lot of changes, you know who to blame / report to
if something breaks.
... and last but not least I've started playing with ocamlbuild.
The myocamlbuild.ml is far from complete now, but it already allows
to build coqtop.{opt,byte} here. See comments at the top of
myocamlbuild.ml, and don't hesitate to contribute, either for completing
or simplifying it !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
glondu
letouzey