aboutsummaryrefslogtreecommitdiff
path: root/configure
AgeCommit message (Collapse)Author
2009-03-22Backport from v8.2 branch of 11986 (interpretation of quantifiedherbelin
hypotheses in induction, unbalanced parenthesis in ltac call stack printer) and 12003 (late update of CREDITS) + update of magic numbers (using a somehow arbitrary value between the 8.2 magic numbers and the possibly forthcoming 8.3 magic numbers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12007 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-17- configure: affiche si le natdynlink est positionnebarras
- coq_makefile: utilise Coq_config pour avoir la liste des contribs - mltop: normalisation des noms de modules ML (majuscule) - Makefiles: introduction de fichiers %-mod.ml qui se chargent de faire les declarations de modules ML d'un plugin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11987 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-11Cleanup: remove unused config/giveostype.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11973 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-11Cleanup: remove old correctness files, unused for a long timeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11971 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Gestion des espaces dans les noms + guess_coqlib sous Windowsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11921 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Fix d'un petit problème de chemin sous Windowsnotin
(cherry picked from commit d2e131c0a013be5cb4674389e42a545f3fbf7b59) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11919 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Fix de divers petits problèmes d'installationnotin
(cherry picked from commit 998a9a62874ba6cf26bdfe28f3ef0c72deaf0c25) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11918 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Report des revisions #11826, #11828 et #11829 de v8.2 vers trunknotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Add -coqtoolsbyteflags and -custom to ./configure...glondu
...and use -custom by default on Windows and MacOS (backport r11895) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11913 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22configure: more adequate message explaining what -opt is doingletouzey
No, -opt has nothing to do with compilation to native or byte-code, nor has it anything to do with the "generation of optimized executables". It simply mean to try to use ocamlc.opt and ocamlopt.opt if they exist. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11837 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Fix d'un petit problème avec ocamlmklib en présence de l'option -camldirnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11834 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-13Updated datesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11782 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-13Workaround to compile the coq archive with dynamic loading on Mac OS 10.5herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11777 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-11- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).herbelin
- Added dependency of mltop.ml4 into config/Makefile (see bug #2023). - Fixed bug #1963 (dependent inversion building a universe-ill-formed conversion problem). - Incidentally, moved "Large non-propositional inductive ..." error message to standard himsg.ml error displayer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11774 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-10Another problem with blanks in filenamesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11773 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-10- Fixed the recompilation of config/revision.ml once every two conmpilations.herbelin
- Fixed an error message in configure - Support for filenames with spaces in coqmktop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11772 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-06Conversion du fichier 'revision' en un fichier .ml + correction d'un bug ↵notin
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
2009-01-06Report de la révision 11754 (compilation sous windows)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11755 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-29compatibility with lablgtk2 version 2.12bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11722 85f007b7-540e-0410-9357-904b9bb8a0f7
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-16Take advantage of natdynlink when available: almost all contribs become ↵letouzey
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
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-14Amélioration du README.doc et de l'installation de la docnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11591 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-10-21More OCaml-3.11-friendly configure scriptglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11487 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-06Install dllcoqrun.so and use it by defaultglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11371 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-06Create the bin/ directory if non-existentglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11369 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-06Always use environment variablesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11368 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-09-05Build coqrun library using ocamlmklib...glondu
...instead of plain ar, so that .so (and .dll) is also created. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11362 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-18Revert commit 11326, to see if it is what makes bench failglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11329 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-08-16Mind environment variables in (generated) coq_config.mlglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11326 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-27Add -browser option to configure scriptglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11271 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24moved magic numbers to configure (share coq/coqchk)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11254 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-16Ajout d'une option pour contrôler l'installation automatique de la ↵notin
documentation + ajout d'un test pour hevea et latex git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11227 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-18Detection de l'architecture sous Windows (et sans uname -o)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11137 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-18Où l'on se débarrasse de uname -onotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11135 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-12Compilation Windowsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11113 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-102-3 petites modifs sur la docnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11091 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09Remplacement des echo -e par printf + bug sur les exécutables ocaml dans ↵notin
coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11079 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-02Petites corrections diverses :herbelin
- bug d'installation (coq_config.cmo était installé une 2ème fois au lieu d'installer coq_config.cmx) - suite nettoyage configure, option reals - ajout d'une option "only parsing" oubliée dans Peano.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11035 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01On cesse de demander une valeur pour l'option reals si l'utilisateurherbelin
n'en donne pas (ça paraît plus simple vu que le temps de compil de reals est devenu mineur, et on fait comme pour fsets qui par défaut est compilé). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11031 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01Quelques amendements liées à la compilation des packages.herbelin
- 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
2008-05-19Fix caml debug flags configuration, -g works with the native compiler onlymsozeau
since 3.10. Fix a bug in classes when the instance database is empty. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10945 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-17Fix a de Bruijn bug in setoid_rewrite when rewriting undermsozeau
a non-dependent product under a lambda. Now qiff can be replaced by a simple setoid_rewrite in NumPrelude. Change configure to not do stripping if compiling with -g... Add -g / CAMLDEBUG flags to the native compilation command too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10941 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-08Integration of theories/Ints into theories/Numbers, again : better ↵letouzey
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
2008-04-19Test pour compilation native camlp5herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10818 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-04Test make 3.81herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10754 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-12 02:00:06 +0000