| Age | Commit message (Collapse) | Author |
|---|
|
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@11977 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
|
|
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
|
|
csdpcert is not meant to be called directly by the user
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11327 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11318 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11211 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In fact, Qge and Ggt disappear, and we only leave notations for > and >=
that map directly to Qlt and Qle.
We also adopt the same approach for BigN, BigZ, BigQ.
By the way, various clean-up concerning Zeq_bool, Zle_bool and similar
functions for Q.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11205 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
test-suites is now bounded -- ensure termination
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11200 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11173 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
le bug #1867
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11086 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
commit de micromega + cache csdp complet.
Quelques questions résiduelles :
- où mettre l'interface entre coq et csdp (csdpcert) ?
- micromega.ml est un fichier engendré par extraction : vaut-il le
coup de compiler coq en deux fois, une 1e fois pour compiler et
extraire micromega.ml, une seconde fois pour inclure micromega.ml ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10955 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"micromega" et "sos" pour les problèmes non linéaires sous-traités à
csdp); mise en place d'un cache pour pouvoir rejouer les preuves
sans avoir besoin de csdp (pour l'instant c'est du bricolage, faudra
affiner cela).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10947 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
setoid_rewrite, et dans Romega.
Pour info, ces fichiers ne sont pas compilés... (?)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
use NRing instead of Ring_polynom.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10264 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
version of Ring_polynom written by Frederic Besson that uses binary trees instead of lists for environments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10240 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
binary positive numbers.
Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7
|
