aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
Commit message (Collapse)AuthorAge
* 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
* CAMLP4DEPS will not work for .byteml and .optmlGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10008 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
| | | | | | | | Removed parsing/lexer.ml4 special case No file depends on pa_extend_m.cmo anymore, Wierd ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: work around gcc bug: lhs of make rule created by -MM does not ↵Gravatar lmamane2007-07-16
| | | | | | include path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10006 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: in C, .d files need to depend on the same as the .o fileGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10005 85f007b7-540e-0410-9357-904b9bb8a0f7
* makefile: dependencies of .c files: assume missing headers are generated filesGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10004 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: use CFLAGS for dependency generation of .c filesGravatar lmamane2007-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10003 85f007b7-540e-0410-9357-904b9bb8a0f7
* A emacs-specific comment to use makefile-mode on Makefile.*Gravatar letouzey2007-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9999 85f007b7-540e-0410-9357-904b9bb8a0f7
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:03:13 +0000