aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts/coqc.ml
Commit message (Collapse)AuthorAge
* Fixed parsing of -no-native-compiler flag.Gravatar mdenes2013-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16141 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqtop -time : display per-command timingsGravatar letouzey2012-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15859 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
| | | | | | | | 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
* No more coqtop.opt, produce directly a coqtop binaryGravatar letouzey2012-08-23
| | | | | | | | | | | 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
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
| | | | | | | | | | | | | | | - 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
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqtop and coqc: cleaning description of options in RefMan and manpages.Gravatar pboutill2012-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
* -user option removalGravatar pboutill2011-11-21
| | | | | | | 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
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* coqc: Recognize option -force-load-proofs.Gravatar letouzey2011-09-15
| | | | | | Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqc: fix the exit codeGravatar letouzey2011-04-15
| | | | | | Patch suggested by Benjamin Monate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
| | | | | | | | | | | | | | | | According to B. Gregoire, this stuff is obsolete. Fine control on when to launch the VM in conversion problems is now provided by VMcast. We were already almost never boxing definitions anymore in stdlib files. "(Un)Boxed Definition foo" will now trigger a parsing error, same with Fixpoint. The option "(Un)Set Boxed Definitions" aren't there anymore, but tolerated (as no-ops), since unknown options raise a warning instead of an error by default. Some more cleaning could be done in the vm. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE argv parsing delegated to coqtopGravatar vgross2010-09-14
| | | | | | | | | | 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
* * scripts/Coqc toplevel/Usage:Gravatar regisgia2010-08-27
| | | | | | Export the -load-proofs officially. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13388 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - 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
* Fixing part 1 of bug #2242 (-I -as and -R -as were supported forGravatar herbelin2010-04-09
| | | | | | coqtop but not coqc). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12911 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqc: on win32, let's call coqtop.exe by default, not coqtop.opt.exeGravatar letouzey2010-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
| | | | | | | | | | | | | | | - 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
* - Suppression date dans configure du trunkGravatar herbelin2008-12-26
| | | | | | | | | - 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
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* - configure: do not strip coqtop on Darwin so as to support dynamic loadingGravatar herbelin2008-12-12
| | | | | | | | | | | - 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
* Fixed bug in VernacExtend printing + missing vernacular printing rules +Gravatar herbelin2008-11-22
| | | | | | | | | | 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
* Tentative d'amélioration de la robustesse des Makefile générés parGravatar notin2008-11-13
| | | | | | | | | | | | | | | | 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
* Suppression d'un warning inutileGravatar notin2008-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11392 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqc: warning de l'option -dump-glob (unused case)Gravatar barras2008-08-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11315 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵Gravatar notin2008-07-18
| | | | | | de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'option -dump-glob et ajout d'une option -no-globGravatar notin2008-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation de l'option -where de coqc avec celle de coqtopGravatar notin2007-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement -no-vm par -vmGravatar herbelin2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7747 85f007b7-540e-0410-9357-904b9bb8a0f7
* compatibility with POWERPCGravatar gregoire2004-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added option -no-vm.Gravatar sacerdot2004-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6254 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction commit precedentGravatar herbelin2004-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6062 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ options coqtop et coqcGravatar herbelin2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqc: create_process sous WindowsGravatar coq2004-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5532 85f007b7-540e-0410-9357-904b9bb8a0f7
* option -l de coqc non reconnue (coq-bugs #509)Gravatar barras2004-03-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5443 85f007b7-540e-0410-9357-904b9bb8a0f7
* option -strict-implicit pas reconnueGravatar barras2003-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option -impredicative-setGravatar herbelin2003-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4829 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage no-strict en -strict-implicit; option -dont-load-proofsGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4540 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion -translate et -ftranslateGravatar herbelin2003-08-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4276 85f007b7-540e-0410-9357-904b9bb8a0f7
* Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofsGravatar herbelin2003-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4254 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du traducteurGravatar desmettr2003-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout options -v7 et -v8, et commandes V7only et V8onlyGravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3407 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
| | | | | | | | | | | - 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
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre erreurs UnixGravatar herbelin2001-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2072 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 03:44:29 +0000