| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15548 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Suppose we declare : Notation foo := bar (compat "8.3").
Then each time foo is used in a script :
- By default nothing particular happens (for the moment)
- But we could get a warning explaining that
"foo is bar since coq > 8.3".
For that, either use the command-line option -verb-compat-notations
or the interactive command "Set Verbose Compat Notations".
- There is also a strict mode, where foo is forbidden : the previous
warning is now an error.
For that, either use the command-line option -no-compat-notations
or the interactive command "Unset Compat Notations".
When Coq is launched in compatibility mode (via -compat 8.x),
using a notation tagged "8.x" will never trigger a warning or error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15438 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15435 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
|
| |
|
|
|
|
|
| |
it is imcompatible with the freedesktop policy that config directory is private.
Feel absolutly free to revert this commit if you think -user should stay
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14713 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
|
| |
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The recent experiment with -dont-load-proofs in the stdlib showed that
this options isn't fully safe: some axioms were generated (Include ?
functor application ? This is still to be fully understood).
Instead, I've implemented an idea of Yann: only load opaque proofs when
we need them. This is almost as fast as -dont-load-proofs (on the stdlib,
we're now 15% faster than before instead of 20% faster with -dont-load-proofs),
but fully compatible with Coq standard behavior.
Technically, the const_body field of Declarations.constant_body now regroup
const_body + const_opaque + const_inline in a ternary type. It is now either:
- Undef : an axiom or parameter, with an inline info
- Def : a transparent definition, with a constr_substituted
- OpaqueDef : an opaque definition, with a lazy constr_substitued
Accessing the lazy constr of an OpaqueDef might trigger the read on disk of
the final section of a .vo, where opaque proofs are located.
Some functions (body_of_constant, is_opaque, constant_has_body) emulate
the behavior of the old fields. The rest of Coq (including the checker)
has been adapted accordingly, either via direct access to the new const_body
or via these new functions. Many places look nicer now (ok, subjective notion).
There are now three options: -lazy-load-proofs (default), -force-load-proofs
(earlier semantics), -dont-load-proofs. Note that -outputstate now implies
-force-load-proofs (otherwise the marshaling fails on some delayed lazy).
On the way, I fixed what looked like a bug : a module type
(T with Definition x := c) was accepted even when x in T was opaque.
I also tried to clarify Subtyping.check_constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
- Due to -top foobar, or -notop, the current dir_path () doesn't
necessary starts by Top.
- Start documenting Ide_intf
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13933 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
Introduces some hacks to have a consistent user experience. When coqtop
prints info on self then exit, return code is 2 if called with
-filteropts, 0 else
For now, no options are accepted by coqide. there is no way for now to
specify a filename that begins with a dash.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
See http://caml.inria.fr/mantis/view.php?id=4940
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13389 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Export the -load-proofs officially.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13388 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12186 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
(cherry picked from commit 998a9a62874ba6cf26bdfe28f3ef0c72deaf0c25)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11918 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 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
|
| |
|
|
|
|
|
|
|
| |
- Utilisation de get_version_date pour l'option -v (plutôt que la date
non à jour du configure)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11714 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
principaux changements sont:
- coqtop (et coqc) maintenant insensible aux variables
d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les
librairies Coq peut être spécifié par l'option -coqlib
- coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et
-camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les
chemins des exécutables OCaml; en dehors du mode boot, coqmktop
cherche les exécutables OCaml dans PATH
- installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci
étant installé en copiant l'architecture des sources (ie lib.cmxa
est installé dans COQLIB/lib/lib.cmxa)
- coq_makefile prend maintenant 3 paramètres sous forme de variables
d'environnement: COQBIN pour dire où trouver les exécutables Coq,
CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les
chemins vers les librairies sont déduits en utilisant -where
Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de
simuler les conditions de la vie réelle (Ocaml pas dans le PATH,
installation binaire relocalisée, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
coq_makefile en présence de fichiers .ml :
- ajout d'une option -config à coqtop qui affiche les informations
de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN,
LOCAL)
- coq_makefile inclut un fichier Makefile.config qui contient les
valeurs des variables sus-mentionnées
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
de coqdoc (compatibilité)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Option -R fait maintenant des Import à tous les niveaux de la
hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche.
- Option -I rend maintenant possible l'accès aux sous-répertoires via
les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il
rend récursivement visibles les noms non qualifiés.
- Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir.
- Ajout option -exclude-dir pour exclure certains sous-répertoires de
la descente récursive de -R.
- Amélioration message de localisation pour fichiers venant d'un "state".
- Adaptation du checker (et ajout du test check_coq_overwriting qui
semblait involontairement oublié dans l'option -R).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
pour inhiber la gestion de Geoproof sous Coqide (qui peut poser des
problèmes avec GTK < 2.6.0)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8932 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6053 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5208 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
- Simplification de strength qui est maintenant un simple drapeau Local/Global.
- Export des catégories de déclarations (Lemma/Theorem/Definition/.../
Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml).
- Export des variables de section initialement associées à une déclaration
(nouveau fichier library/dischargedhypsmap.ml).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
fichier usage incorrect (libdir et bindir ont disparu)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2629 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2519 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2495 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1984 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1612 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1552 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
standard pour associer un nom physique à un nom logique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1066 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
- coqc -v réparé
- coqtop: options -byte et -opt
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@940 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@915 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7
|
letouzey
herbelin
pboutill
glondu
vgross
regisgia
msozeau
notin
barras
filliatr
courant