aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
Commit message (Collapse)AuthorAge
* Remplacement des 'cp' et 'mkdir' par 'install'Gravatar notin2008-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11112 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2-3 petites modifs pour la compilation sous Windows...Gravatar notin2008-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11062 85f007b7-540e-0410-9357-904b9bb8a0f7
* Copie des .cmi en plus des .cma et des .cmxaGravatar notin2008-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
| | | | | | | | | | Debug handling of identifiers in coqdoc (should work with modules and sections) and add missing macros. Move theories/Program to THEORIESVO to put the files in the standard library documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petites corrections diverses :Gravatar herbelin2008-06-02
| | | | | | | | | | | - 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
* Quelques amendements liées à la compilation des packages.Gravatar herbelin2008-06-01
| | | | | | | | | | | | | | | | | | | | | - 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
* Fix last commit about revision: I'm unsure about the role of "set -e", Gravatar letouzey2008-05-31
| | | | | | | | but it probably works only if placed in front of the shell line git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attempt to avoid killing+recreating the file revision with same content.Gravatar letouzey2008-05-31
| | | | | | | | This should prevent some useless coqtop+theories recompilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11025 85f007b7-540e-0410-9357-904b9bb8a0f7
* the -g option is not recongnized in ocaml < 3.10.0Gravatar jforest2008-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10984 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed dependency problems with the checkerGravatar barras2008-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10970 85f007b7-540e-0410-9357-904b9bb8a0f7
* improved coqchk targetsGravatar barras2008-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10963 85f007b7-540e-0410-9357-904b9bb8a0f7
* added coqchk to the main Makefile and a make variable VALIDATE to check the ↵Gravatar barras2008-05-22
| | | | | | vo files of the theories git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10962 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrections d'erreurs rapportées par Frédéric Besson sur le précédentGravatar herbelin2008-05-20
| | | | | | | | | | | | | | 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
* Intégration de micromega ("omicron" pour fourier et sa variante sur Z,Gravatar herbelin2008-05-19
| | | | | | | | | | | "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
* Fix caml debug flags configuration, -g works with the native compiler onlyGravatar msozeau2008-05-19
| | | | | | | 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
* Fix a de Bruijn bug in setoid_rewrite when rewriting underGravatar msozeau2008-05-17
| | | | | | | | | | 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
* Integration of theories/Ints into theories/Numbers, again : better ↵Gravatar letouzey2008-05-08
| | | | | | | | | | | | 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
* Integration of theories/Ints into theories/Numbers, part 3: auto-generation ↵Gravatar letouzey2008-05-08
| | | | | | of NMake.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10902 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration of theories/Ints into theories/Numbers, part 1: moving filesGravatar letouzey2008-05-07
| | | | | | | | | | | | | | For the moment, the Ints files are simply moved into directories in theories/Numbers with meaningful names. No filenames changed, apart from: Zaux.v -> theories/Numbers/BigNumPrelude.v MemoFn.v -> theories/Lists/StreamMemo.v More to come... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10899 85f007b7-540e-0410-9357-904b9bb8a0f7
* Calcul plus robuste du numéro de révision (ne marche en positionnantGravatar herbelin2008-04-29
| | | | | | | | | | | LANG que si LC_ALL n'est pas lui-même défini) --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M Makefile.build git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans coq_makefile: génération des règles implicites ↵Gravatar notin2008-04-29
| | | | | | en présence de l'option -custom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10869 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation bug de compil introduit au precedent commitGravatar jforest2008-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10866 85f007b7-540e-0410-9357-904b9bb8a0f7
* first-order --> firstorder (kills a warning about not being a valid id)Gravatar letouzey2008-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10805 85f007b7-540e-0410-9357-904b9bb8a0f7
* migration of the old IntMap library from StdLib to a user contrib ↵Gravatar letouzey2008-03-19
| | | | | | (Cachan/IntMap) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various improvements of coqdep, resulting in a big speedupGravatar letouzey2008-03-19
| | | | | | | | | | | | | | | | | | | | * use of Hashtbl for large sets/maps * reorganisation of directory-traversal functions, in order to avoid redundant stat / open * all files and directory whose names start by . are skipped while tranversing directories: no more visits of .svn ! * new option -boot to be used when computing dependencies of the stdlib: - no need in this case to records the system .vo in coqlibKnown - add directly inside coqdep the equivalent of -R theories Coq and -R contrib Coq As a result, coqdep'ing all the .vo of the stdlib now takes 25s on my machine instead of 2min30 earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10695 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout cible programs comme synonyme de subtacGravatar herbelin2008-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10683 85f007b7-540e-0410-9357-904b9bb8a0f7
* New option -glob for coqdep, in order to avoid nasty tricks with sed in MakefileGravatar letouzey2008-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10668 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: correction de l'appel aux exécutables OcamlGravatar notin2008-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plongement de doc/Makefile dans la nouvelle architecutre des MakefileGravatar notin2008-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implement KEEP_ML4_PREPROCESSED option in build systemGravatar lmamane2008-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implement NO_RECALC_DEPS option in build systemGravatar lmamane2008-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10560 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration de la génération des graphes de dépendancesGravatar notin2008-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10438 85f007b7-540e-0410-9357-904b9bb8a0f7
* migration of ide/utf8.v to theories/Unicode/Utf8.vGravatar letouzey2007-12-13
| | | | | | | | | | | | | | | | | | These notations aren't CoqIDE-specific, I can now use them with ProofGeneral (after a small modification of PG, contact me if you're interested by the patch). So let's place this file in a globally visible subdir of theories/. By the way, the filename is now uppercase as all other .v files. By the way, minor other changes in Makefile : extraction/test doesn't exist anymore, and tags / otags can be made without re-doing any find. NB: be sure to use etags that comes from emacs and not the one of exuberant-ctags, since the latter has now a different syntax (in debian, see update-alternatives etags). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1741Gravatar notin2007-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intallation des .cma/.cmxaGravatar notin2007-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Copie des .cma et des .cmxa, et de grammar.cma dans le répertoire de Coq ↵Gravatar notin2007-10-18
| | | | | | (pour faciliter la compilation des tactiques ml par les utilisateurs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10238 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow a few build system optimisations/corner-cuttingGravatar lmamane2007-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10218 85f007b7-540e-0410-9357-904b9bb8a0f7
* Calcul des dependances sous WindowsGravatar notin2007-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10196 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1715Gravatar notin2007-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10183 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option -lablgtkdir au configure (basé sur patch de GuillaumeGravatar herbelin2007-10-04
| | | | | | | | Rousse -- rapport de bug #1713) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compilation sous windowsGravatar notin2007-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10171 85f007b7-540e-0410-9357-904b9bb8a0f7
* Preventing gcc to generate dependencies wrt OCaml files (otherwise, we run ↵Gravatar notin2007-10-02
| | | | | | into troubles under Windows) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10166 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
| | | | | | | | | | | | | | 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
* Makefile: Revert r10015, which was based on a misunderstandingGravatar lmamane2007-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: needs GNU Make 3.81Gravatar lmamane2007-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: more robustness all aroundGravatar lmamane2007-07-18
| | | | | | | | - Make sure make notices when a command fails - don't leave behind half-baked output files of commands that failed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: Do _not_ delete dummy .ml files of .ml4 files even when not needed ↵Gravatar lmamane2007-07-17
| | | | | | anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: -MG doesn't (and can't) do what is necessaryGravatar lmamane2007-07-16
| | | | | | | | | | | | | | The -MG option causes gcc to add any non-found .h file verbatim in the dependencies. This naturally doesn't include the path to it (because the path is unknown) and thus make doesn't know how to build it; it knows how to build kernel/byterun/coq_jumptbl.h, not "coq_jumptbl.h". --This line, and those below, will be ignored-- M Makefile.common M Makefile.build git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10011 85f007b7-540e-0410-9357-904b9bb8a0f7
* A cleaner solution to "make deletes .ml4.d files -> infinite loop" problemGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups... empty .ml4.d files producedGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10009 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:33:59 +0000