| Commit message (Collapse) | Author | Age |
... | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11370 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
The environment variable COQTOP has a different meaning for Coq
executables and for Coq Makefiles, which is troublesome when make
forwards it to subprocesses via the environment.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11366 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11328 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Correction divers messages d'erreur
- lorsque rien à réécrire dans une hyp,
- lorsqu'une variable ltac n'est pas liée,
- correction anomalie en présence de ?id dans le "as" de induction,
- correction mauvais env dans message d'erreur de unify_0.
- Diverses extensions et améliorations
- "specialize" :
- extension au cas (fun x1 ... xn => H u1 ... un),
- renommage au même endroit.
- "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize".
- "induction"
- intro des IH toujours au sommet même si induction sur var quantifiée,
- ajout d'un hack pour la reconnaissance de schémas inductifs comme
N_ind_double mais il reste du boulot pour reconnaître (et/ou
réordonner) les composantes d'un schéma dont les hypothèses ne sont pas
dans l'ordre standard,
- vérification de longueur et éventuelle complétion des
intropatterns dans le cas de sous-patterns destructifs dans induction
(par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas
le n dans le contexte),
- localisation des erreurs d'intropattern,
- ajout d'un pattern optionnel après "as" pour forcer une égalité et la
nommer (*).
- "apply" accepte plusieurs arguments séparés par des virgules (*).
- Plus de robustesse pour clear en présence d'evars.
- Amélioration affichage TacFun dans Print Ltac.
- Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu
(incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !).
- Fusion VTactic/VFun dans l'espoir.
- Mise en place d'un système de trace de la pile des appels Ltac (tout en
préservant certains aspects de la récursivité terminale - cf bug #468).
- Tactiques primitives
- ajout de "move before" dans les tactiques primitives et ajout des
syntaxes move before et move dependent au niveau utilisateur (*),
- internal_cut peuvent faire du remplacement de nom d'hypothèse existant,
- suppression de Intro_replacing et du code sous-traitant
- Nettoyage
- Suppression cible et fichiers minicoq non portés depuis longtemps.
(*) Extensions de syntaxe qu'il pourrait être opportun de discuter
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- typo du configure;
- warnings variables non utilisées dans ide/utils;
- suppression des variables vides COQINSTALLPREFIX et OLDROOT parce
que l'option -e que l'on aurait pu en principe utiliser pour les
surcharger ne fonctionne pas lorsqu'il y a plusieurs niveaux
d'imbrication de makefiles (comme c'est le cas quand on vient
du makefile servant à faire les packages qui appelle le makefile
principal qui appelle les makefile.stage);
- utilisation de ALLVO plutôt qu'un find pour trouver les .v sur
lesquels appliquer coqdep (permet d'éviter des warning sur les fichiers
de test, non prévus pour faire partie de la biblio standard);
- utilisation de -custom sur les bytecode qui ne l'étaient pas encore
(coqchk et coqmktop) pour être indépendant de ocamlrun à
l'installation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11029 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
.v.d are created exactly for all $(VFILES), which was only a
"find -name .v", so $(GENVFILES) should be added to $(VFILES)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10965 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
generation of NMake.v
- genN.ml becomes NMake_gen.ml
- no need to produce the corresponding binary: we use ocaml NMake_gen.ml > NMake.v
- beware! redoing a ./configure is mandatory after this commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10903 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
of NMake.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10902 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
fichiers emacs ouverts au moment de la création des dépendances
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10519 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10438 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
These notations aren't CoqIDE-specific, I can now use them with
ProofGeneral (after a small modification of PG, contact me if you're
interested by the patch). So let's place this file in a globally
visible subdir of theories/. By the way, the filename is now uppercase
as all other .v files.
By the way, minor other changes in Makefile : extraction/test doesn't
exist anymore, and tags / otags can be made without re-doing any find.
NB: be sure to use etags that comes from emacs and not the one of
exuberant-ctags, since the latter has now a different syntax
(in debian, see update-alternatives etags).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10376 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
target already exists
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10223 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10218 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
recommended way more explicitly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10050 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
standard:
- ajout d'une entrée dans le Makefile principal pour le fichier de
globalisations glob.dump
- modifications de doc/Makefile et de l'index html pour gérer les
nouveaux fichiers de la librairie standard (en part. ceux dans
Ints)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10025 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
|