| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15770 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15769 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15767 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
We now always produce two binaries, coqtop and coqtop.byte :
- If ocamlopt is available, coqtop is directly what used to be coqtop.opt,
no more symlinks needed.
- Otherwise, coqtop is a copy of coqtop.byte.
The same for coqchk and coqide...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14903 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Add option -boot to the coqtop given to fake_ide
- Be sure that a dying coqtop subprocess cannot go unnoticed.
Before that, for repositories compiled without -local,
coqtop -ideslave was dying immediately because it was missing
its coqlib informations. Then the first command send via
Marshal.to_channel was triggering a SIGPIPE and hence the death
of fake_ide. Strangely, the return code was not necessarily
understood as non-zero (?!). We now catch SIGPIPE and do an
"exit 1".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14480 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After a successful build, re-doing make world should almost do nothing.
For that:
- Many targets added to .PHONY, especially "tools" since a "tools"
directory exists. And anyway this is said to speed-up make a bit.
- Concerning fake_ide, mentionning the .cm* instead of the .ml*
avoid rebuilding these .cm*, and hence possibly many other things.
- in Makefile.doc: fix the rule building index_url.txt
- coqtop.* is now built by $(BESTCOQMKTOP) instead of $(COQMKTOP)
(which is the symlink). This avoids a situation where a first
"make" could redo just a few files while a second "make" will
rebuild many more. Typical scenario : touch the Makefile,
1st make was re-doing tolink.ml and then coqmktop, but no more,
a 2nd make was then detecting that coqtop and the stdlib was to
be redone
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- make clean really erases *.log
- some missing \n at end of files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
This way, we can test each night that coqtop -ideslave handles
correctly some specific sequences of API calls.
For the moment, we add a few tests of the backtracking.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14456 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14233 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13805 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
The test misc/deps-order was failing in non-local mode.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13560 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13495 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
coqdep since it is now deterministic (later -R's overwriting former ones).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13055 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13052 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12963 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
...so that "./check > check.log" works as expected.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12933 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12925 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Using a Makefile for tests allows (easily) running them in parallel,
running and/or benching a single one, adding depedencies between them,
and running them with a version of Coq different than the one compiled
with the current source tree. The new way to make statistics about
successes/failures is also more reliable (I found bugs in the previous
one).
Statistics (on AMD Phenom(tm) 9950 Quad-Core Processor 2.6 GHz):
- plain sh script: ~ 3 min
- make -j6: ~ 1 min
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12921 85f007b7-540e-0410-9357-904b9bb8a0f7
|