aboutsummaryrefslogtreecommitdiff
path: root/scripts
AgeCommit message (Collapse)Author
2008-12-26- Suppression date dans configure du trunkherbelin
- 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
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
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
2008-12-12- configure: do not strip coqtop on Darwin so as to support dynamic loadingherbelin
- configure: remove useless newline (hoping it is OK for everyone) - coqc: added option -no-glob in accordance with coqc -usage - coq_makefile: support for installation of all .cmo and all .cmxs in user-contrib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11676 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-19Execute #rectypes directive in embedded OCaml toplevel...glondu
...to avoid the need to have cflags.cmi around. This directive will likely be available in the next version of OCaml. See OCaml bug #4460. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11605 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-13Tentative d'amélioration de la robustesse des Makefile générés parnotin
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
2008-10-29Remove calls to Dynlink.add_{interfaces,available_units} altogetherglondu
According to OCaml's Changes, all modules loaded so far (and statically linked) are available to dynamically loaded modules (since 3.07). Therefore, these calls seem irrelevant now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11522 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-28Native "Declare ML Module" when possibleglondu
Dynlink.add_{interfaces,available_units} are deprecated and not implemented natively. Currently, native "Declare ML Module" doesn't work because of this. Dynlink-related should be switched to the API introduced in OCaml 3.07. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11518 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-09Suppression d'un warning inutilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11392 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-05Parametrize link flags for VM-dependent bytecodeglondu
* Remove unneeded -custom flags. * Replace needed ones by a configure parameter. Setting it to "-dllib -lcoqrun" enables the creation/usage of pure bytecode executable provided the so/dll with the VM is found by ocamlrun. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11363 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-07coqc: warning de l'option -dump-glob (unused case)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11315 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵notin
de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-08forgotten debug printf in coqmktop (anyway, can be obtained by -echo)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11215 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-24Suppression de l'option -dump-glob et ajout d'une option -no-globnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-19Intégration de micromega ("omicron" pour fourier et sa variante sur Z,herbelin
"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
2008-03-09Des choses bizarres avec pa_op.cmo (extension syntaxique pour parser)herbelin
se passent avec camlp5 qui ne se passaient pas avec l'ancien camlp4: pa_op.cmo exige camlp5o.cma mais alors, il y a un message de redéfinition de ipatt que je ne sais pas éviter avec coqtop.byte. Puisque pa_op.cmo n'est finalement pas utile, on le retire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10646 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-06Oups. Clflags.recursive_types isnt normally accessible on a standard ocaml ↵letouzey
installation. Backtrack for the moment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10292 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-05For debugging with coqtop.byte with ocaml 3.10, the toplevel should be made ↵letouzey
with -rectypes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10288 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-18Uniformisation de l'option -where de coqc avec celle de coqtopnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10235 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-29Plus d'option -v8 dans coqmktopherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9813 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-17Correction bug #1282herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9495 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-14Modification de l'appel aux exécutables Camlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9135 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Suite ajout option -ocamlib à configurenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9115 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-29Compilation de Coq sous Windowsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9098 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-04- intégration de la modification suggérée par L. Mamane: coqmktop passe ↵notin
maintenant aussi l'option -dtypes à ocamlmktop - ajout d'une variable USERFLAGS, permettant à un utilisateur de rajouter facilement des options de compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8787 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28Remplacement -no-vm par -vmherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7747 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-04Passage option -w à ocamlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7513 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18q_*.cmo useless for making coqtopherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6734 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22compatibility with POWERPCgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-15bug coqmktop avec libcoqrun.a en bytecodebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6301 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-25Added option -no-vm.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6254 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-26no-assert en mode natifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6137 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-04Correction commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6062 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03MAJ options coqtop et coqcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6053 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-18coqc: create_process sous Windowscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5532 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-09option -l de coqc non reconnue (coq-bugs #509)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5443 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-26deplacement des cma et cmxa dans les sous-repertoiresbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5249 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-14make libraries, lexing of more utf8 symbolsmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5201 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-30option -strict-implicit pas reconnuebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5162 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-30ameliorations coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Ajout option -impredicative-setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4829 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Renommage no-strict en -strict-implicit; option -dont-load-proofsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4540 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Inclusion automatique de highparsingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4384 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:33:25 +0000