aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
Commit message (Collapse)AuthorAge
* Suppression de la dépendance de install-doc envers doc :Gravatar notin2008-10-17
| | | | | | | | | | - make install ne compile plus la doc - make world compile la doc (sauf si option --with-doc no) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalize usage of $(FIND_VCS_CLAUSE) and add debian to itGravatar glondu2008-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not install csdpcert in $(BINDIR)Gravatar glondu2008-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11388 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add some calls to $(STRIP) for consistencyGravatar glondu2008-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11378 85f007b7-540e-0410-9357-904b9bb8a0f7
* $(DLLCOQRUN) is not an executableGravatar glondu2008-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11377 85f007b7-540e-0410-9357-904b9bb8a0f7
* Install dllcoqrun.so and use it by defaultGravatar glondu2008-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11371 85f007b7-540e-0410-9357-904b9bb8a0f7
* $(COQLIB) -> $(COQLIBINSTALL) in MakefilesGravatar glondu2008-09-06
| | | | | | | COQLIB has a special meaning to executables, and we don't want make to set it to a path surrounded by double quotes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use $(COQTOPEXE) to refer to bin/coqtop in MakefilesGravatar glondu2008-09-06
| | | | | | | | The environment variable COQTOP has a different meaning for Coq executables and for Coq Makefiles, which is troublesome when make forwards it to subprocesses via the environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parametrize link flags for VM-dependent bytecodeGravatar glondu2008-09-05
| | | | | | | | | * 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
* Build coqrun library using ocamlmklib...Gravatar glondu2008-09-05
| | | | | | ...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
* Rely on ocamlc to call the C compiler...Gravatar glondu2008-09-04
| | | | | | | | | | | ...with proper options for dynamic loading of C stubs. I believe this is the preferred way of compiling C stubs. It also adds by itself -fno-defer-pop, -Wall, -I `ocamlc -where`, so CFLAGS could also be simplified. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11358 85f007b7-540e-0410-9357-904b9bb8a0f7
* added Makefile target: validate (to recheck all .vo in a row)Gravatar barras2008-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11347 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo (corrige le bug #1928)Gravatar notin2008-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming parser -> coq-parserGravatar glondu2008-08-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Install csdpcert with librariesGravatar glondu2008-08-16
| | | | | | csdpcert is not meant to be called directly by the user git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11327 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix build/install failures when ocamlopt is not availableGravatar glondu2008-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use COQINSTALLPREFIX for doc tooGravatar glondu2008-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove pcoq from check prerequisitesGravatar glondu2008-07-28
| | | | | | | | It is already built by world, and this way, "make -j3 check" from clean sources work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11283 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de cibles pour le manuel de référence (refman-nodep, stdlib-nodep, ↵Gravatar notin2008-07-16
| | | | | | refman-quick) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11229 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option pour contrôler l'installation automatique de la ↵Gravatar notin2008-07-16
| | | | | | 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
* Installation de la documentationGravatar notin2008-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11174 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-03 11:00:35 +0000