| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The idea was to allow rebuilding coqtop without the whole stdlib,
but it's not working anymore since the stdlib also depends on
plugins .cmxs, hence its compilation will be triggered anyway.
Since I've no idea how to restore the old behavior (except via
hacking the output of coqdep with more ORDER_ONLY hack), I simply
declare this option dead, and remove it for improving clarity.
NB: an imperfect workaround is to touch all the .vo after rebuilding
coqtop and the plugins...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15823 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
For starting a bare coqtop, the recommended option is now "-noinit"
that skips the load of Prelude.vo. Option "-nois" is kept for
compatibility, it is now an alias to "-noinit".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 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@15366 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15255 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
but it requires otags-3.12.2 and and ./configure -usecamlp4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15147 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
|
|
|
|
|
|
|
|
| |
No need for a distclean rule in test-suite, since the root-level distclean
already launches clean, which launches clean in test-suite, and this one
does the job
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14915 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@13976 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13404 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
divers corrections sur la génération du manuel de référence.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13186 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13052 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
dev/ocamldoc/
old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)
"make clean" cleans dev/ocamldoc/ properly
wierd? calls of dependency graph generation leave unchanged
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 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
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- avoid recomputing CAMLP4DEPS in the %.ml:%.ml4 rule
- a macro for compiling the tools by the best ocaml compiler
- use of $(if ...) rather that $ifdef
- some variables of Makefile.common were not that useful
(e.g. $(COQCCMX), which is $(COQCCCMO:.cmo=.cmx), used only once)
- the build of coqc.* should not depend upon coqtop, only its launch
(or I'm missing something)
- useless $(CAMLP4EXTENDFLAGS) variable
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12846 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
dev/doc/build*.txt
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12840 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Instead of the separate stage mechanism, we let make handle the
build and inclusion of all .d. Some initial calls to camlp4o
will fail, but make tries again later, and this finally works
great. These initial error message are made nice to avoid bad
interaction with M-x next-error
- The only recursive call to a sub-make is Makefile calling Makefile.build
in which the includes of .d take place. This allows to avoid compiling
anything for a make clean or make tags
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12839 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- We clarify their definition via some custom make function: find, diff...
- We avoid duplications via some $(sort ...)
- Some name changes:
* old $(MLFILES) now corresponds to $(MLSTATICFILES) (but .ml from
.mly and .mll aren't in it anymore).
* new $(MLFILES) contains all .ml, either static or generated from
.mly .mll .ml4 or _mod.ml made out of .mllib
* $(ML4FILESML) is now $(GENML4FILES)
...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12836 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
*.dep.ps for svn
the syntax for find is sooo intuitive ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12835 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- This way, the Makefile.build gets shorter and simplier, with a few nasty
hacks removed.
- In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep".
Instead, we now use ocamldep -modules, and process its output via coqdep_boot.
This ways, *.cm* of .ml4 are correctly located, even when some .ml files
aren't generated yet.
- There is no risk of editing the .ml of a .ml4 by mistake, since it is by
default in a binary format (cf pr_o.cmo and variable READABLE_ML4).
M-x next-error still open the right .ml4 at the right location.
- mltop.byteml is now mltop.ml, while mltop.optml keeps its name
- .ml of .ml4 are added to .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12818 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12690 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
It has moved to the contribs (Sophia-Antipolis/Interface).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12349 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
|
|
|
|
|
|
| |
clean
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12047 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
.bzr files (Bazaar management files) in VCS clause (see 12043 in v8.2
branch).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12044 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12016 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11994 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11988 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
build stages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* I encountered error messages during compilation, for instance
ocamlopt complaining about non-existing coq_config.cmi when compiling
coq_config.ml. Moreover, make was _not_ stopping at these errors
(WTF?!). After some debug, it turned out to be (indirectly) my fault:
I placed earlier the inclusion of the new .mllib.d in
Makefile.stage1, but this is too early, coqdep, which is used to
compute these files, isn't built yet. Due to the semantics of
"-include", make tries to build it, fails with the above error,
and goes on happily. Arrgh. After moving the inclusion of these
.mllib.d to Makefile.stage2, everything seems to work ok now.
* Since we're using such "nice" non-trivial features of make, I've
started a small FAQ section about them at the beginning of Makefile
* Recursive calls to make are now done with two options:
--no-builtin-rules : let's avoid builtin rules like "%:%.o" ...
--warn-undefined-variable : using a non-defined variable isn't
necessarily bad, but I found a few bugs with this option, and
I suggest we keep it.
* Clarified the rules about stage* in Makefile and their
STAGE*_TARGETS variables in Makefile.common. Now a newcomer _might_
have a chance to grasp in less than a day what's going on ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11983 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Overloading of GPack.notebook => Vector no longer needed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11952 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11911 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11909 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
(which allows to get rid of '-type f' hack)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11757 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
dans le configure introduit par les révisions 11754 et 11755
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11756 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
loadable plugins
- Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode).
- Features that were available without any Require are now loaded systematically
when launching coqtop (see Coqtop.load_initial_plugins):
extraction, jprover, cc, ground, dp, recdef, xml
- The other plugins are loaded when a corresponding Require is done:
quote, ring, field, setoid_ring, omega, romega, micromega, fourier
- I experienced a crash (segfault) while turning subtac into a plugin, so this
one stays statically linked into coqtop for now
- When the ocaml version doesn't support natdynlink, or if "-natdynlink no"
is explicitely given to configure, coqtop is statically linked with all of
the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear.
- How should coqdep handle a "Declare ML Module "foo"" if foo is an archive
and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the
same location as the .v during the build, but can be moved later in any place of
the ml loadpath.
This is clearly an experimentation. Feedback most welcome...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11666 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11390 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11389 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11388 85f007b7-540e-0410-9357-904b9bb8a0f7
|