From 42c6994226a1069867b0994c0d9b864b94f2aa94 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 28 Jul 2019 16:45:07 -0500 Subject: [PATCH 1/4] delete unnecessary files --- AFAIRE.txt | 22 ------------------ README.txt | 29 ----------------------- To_do.txt | 65 ---------------------------------------------------- alltex.sh | 9 -------- make_make | 6 ----- make_project | 3 --- 6 files changed, 134 deletions(-) delete mode 100644 AFAIRE.txt delete mode 100644 README.txt delete mode 100644 To_do.txt delete mode 100755 alltex.sh delete mode 100755 make_make delete mode 100644 make_project diff --git a/AFAIRE.txt b/AFAIRE.txt deleted file mode 100644 index fcb5e1d..0000000 --- a/AFAIRE.txt +++ /dev/null @@ -1,22 +0,0 @@ -Certains exos placés dans depprod (à la création du site) ont maintenant -leur énoncé dans le chapitre "everyday logic". -Il faudra séparer ces exos en une partie "terme de preuve" (depprod) -et une partie "tactiques" (everyday). -Mais ça ne me parait pas très urgent -(Pierre, le 31 Octobre 2003). - ------------------------------------------------------------------------------ -Eviter d'avoir des fichiers toto.html pour un module toto.v - -Possibilités : a) noms "about_toto.html" - ou b) sous-répertoire HTML -Problème : boulot de Romain : - références croisées + cvs delete/add - -Faire ça tranquillement : - de façon non destructive (on ne détruira les anciens fichiers que - lorsque tout sera doublé). - -Meilleure solution: changement de coq_makefile - ----------------------------------------------------------------------- \ No newline at end of file diff --git a/README.txt b/README.txt deleted file mode 100644 index 8b6cab4..0000000 --- a/README.txt +++ /dev/null @@ -1,29 +0,0 @@ - -Some files can work only with coqCVS - - They are either in subdirectories */CVSONLY - or in */SRC, but compilable with make -f makeCVS all - - - - - -Some files can work only with coqV8 (the official version) - - They are either in subdirectories */V8ONLY - or in */SRC, but compilable with make -f makev8 all - - -Other files can work indifferently with one version aor another. -use the "standard" makefile - - - - -For testing all files : - - with coqV8, "make test" - - with coqCVS, "make testCVS" - - diff --git a/To_do.txt b/To_do.txt deleted file mode 100644 index 5e55bbe..0000000 --- a/To_do.txt +++ /dev/null @@ -1,65 +0,0 @@ -AFAIRE.txt - -Voir les entiers int31 (Admitted dans Powers.v) - - -A faire : Rédiger une note sur le travail à faire sur les corrigés; - enlever des auto, tauto, congruence, now, ";", etc. - rubrique "implicit exercises" ci-dessus + en cas de définitions différentes - de la meme notion essayer d'en prouver l'équivalence. - -Plein de truc sur les ordres, permutations, tris à factoriser ou cross référencer. - - -Note sur les fichiers chap$i$.v . Contiennent pour des raisons pédagogiques - des Abort, Restart, Undo, Check, Print, etc... Ok pour PFG, pour CoqIde ???? - -Ajouter un exo : -Comparer les preuves utilisant les différentes définitions de la fermeture transitive. -En quoi ça change la preuve de bonne fondation de R+ ? - -chapitre 2 : Transformer en "Coq as a Programming Language" + exos des Summer Schools - -ch2_types_expresssions/Zbtree.html : -Explicit the links at the bottom of the page -ch2_types_expresssions/SRC/Zbtree.v Create exercises on Zbtree_rec[t] - - -contents.html -index.html -README.txt - -. -./ch6_inductive_data/SRC: -vectorsbis.v (nettoyer, puis mettre avec le tutorial avec Eduardo) -Faire un html sur Computing_powers - - -./ch7_automatic_tactics: -index.html - -On_nstaz.v A faire - -./ch8_inductive_predicates: -index.html -parsing.tex - -./ch8_inductive_predicates/SRC: -id_solution.v misplaced? Add something about non empty vectors -magaud.v OK mettre une référence vers ce fichier: message envoyé à Nicolas - - -.Add a link to SRC/even_odd.v - -index.html -plus_prim.html Move to another chapter! - - -./tutorial_inductive_co_inductive_types: -J'ai fait une copie : coqart/trunk/Coqbook/IndTutorialV8.5 - la vérifier et en même temps faire le RecTutorial.v cohérent -RecTutorial.v (fait en partie : jusqu a le_case_analysis (14%) ) - -./tutorial_type_classes: -Faire un README - diff --git a/alltex.sh b/alltex.sh deleted file mode 100755 index bae10ec..0000000 --- a/alltex.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/bash -function parcours () -{ -for f in $1/SRC/*.v; do - local texname=`dirname $f`"/"`basename $f ".v" `".tex"; - if test ! -e $texname ;then touch $texname ; fi; done -} - -parcours $1 diff --git a/make_make b/make_make deleted file mode 100755 index f4d70aa..0000000 --- a/make_make +++ /dev/null @@ -1,6 +0,0 @@ -echo "-R . coqart89" >_CoqProject ; find . -name '*.v' -print >> _CoqProject; echo 'COQDOCEXTRAFLAGS = "-interpolate --gallina -utf8 --latex --html"' >> _CoqProject - -coq_makefile -f _CoqProject -o Makefile - - - diff --git a/make_project b/make_project deleted file mode 100644 index 06605f9..0000000 --- a/make_project +++ /dev/null @@ -1,3 +0,0 @@ -echo "-R . coqart85 " >_CoqProject ; find . -name '*.v' -print >> _CoqProject; echo 'COQDOCFLAGS = "-interpolate -utf8 --latex --html --body-only --short"' >> _CoqProject - - From 24f4777d9d4e69e0dd0de5e184d37c2d5af70019 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 28 Jul 2019 16:45:57 -0500 Subject: [PATCH 2/4] metadata and files generated from template --- .travis.yml | 52 +++++++++++++++++++++++++ README.md | 98 ++++++++++++++++++++++++++++++++++++++++++++++++ coq-coq-art.opam | 32 ++++++++++++++++ default.nix | 25 ++++++++++++ meta.yml | 88 +++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 295 insertions(+) create mode 100644 .travis.yml create mode 100644 README.md create mode 100644 coq-coq-art.opam create mode 100644 default.nix create mode 100644 meta.yml diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 0000000..0b3f804 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,52 @@ +opam: &OPAM + language: minimal + sudo: required + services: docker + install: | + # Prepare the COQ container + docker pull ${COQ_IMAGE} + docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} ${COQ_IMAGE} + docker exec COQ /bin/bash --login -c " + # This bash script is double-quoted to interpolate Travis CI env vars: + echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\" + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex # -e = exit on failure; -x = trace for debug + opam update -y + opam pin add ${CONTRIB_NAME} . -y -n -k path + opam install ${CONTRIB_NAME} -y -j ${NJOBS} --deps-only + opam config list + opam repo list + opam list + " + script: + - echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r' + - | + docker exec COQ /bin/bash --login -c " + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex + sudo chown -R coq:coq /home/coq/${CONTRIB_NAME} + opam install ${CONTRIB_NAME} -v -y -j ${NJOBS} + " + - docker stop COQ # optional + - echo -en 'travis_fold:end:script\\r' + +nix: &NIX + language: nix + script: + - nix-build --argstr coq-version-or-url "$COQ" --extra-substituters https://coq.cachix.org --trusted-public-keys "cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= coq.cachix.org-1:5QW/wwEnD+l2jvN6QRbRRsa4hBHG3QiQQ26cxu1F5tI=" + +matrix: + include: + + # Test supported versions of Coq via Nix + - env: + - COQ=8.9 + <<: *NIX + + # Test supported versions of Coq via OPAM + - env: + - COQ_IMAGE=coqorg/coq:8.9 + - CONTRIB_NAME=coq-coq-art + - NJOBS=2 + <<: *OPAM + diff --git a/README.md b/README.md new file mode 100644 index 0000000..fcbe356 --- /dev/null +++ b/README.md @@ -0,0 +1,98 @@ +# Coq'Art + +[![Travis][travis-shield]][travis-link] +[![Contributing][contributing-shield]][contributing-link] +[![Code of Conduct][conduct-shield]][conduct-link] +[![Gitter][gitter-shield]][gitter-link] +[![DOI][doi-shield]][doi-link] + +[travis-shield]: https://travis-ci.com/coq-community/coq-art.svg?branch=master +[travis-link]: https://travis-ci.com/coq-community/coq-art/builds + +[contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg +[contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md + +[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg +[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md + +[gitter-shield]: https://img.shields.io/badge/chat-on%20gitter-%23c1272d.svg +[gitter-link]: https://gitter.im/coq-community/Lobby + +[doi-shield]: https://zenodo.org/badge/DOI/10.1007/978-3-662-07964-5.svg +[doi-link]: https://doi.org/10.1007/978-3-662-07964-5 + +Coq'Art is the familiar name for the first book on the Coq proof assistant +and its underlying theory, the Calculus of Inductive Constructions. +This project contains the source of all examples and the solution to 170 +out of over 200 exercises from the book. + + + +## Meta + +- Author(s): + - Yves Bertot (initial) + - Pierre Castéran (initial) +- Coq-community maintainer(s): + - Yves Bertot ([**@ybertot**](https://github.com/ybertot)) + - Pierre Castéran ([**@Casteran**](https://github.com/Casteran)) +- License: [CeCILL-B](LICENSE) +- Compatible Coq versions: 8.9 +- Additional Coq dependencies: none + +## Building and installation instructions + +The easiest way to install the latest released version of Coq'Art +is via [OPAM](https://opam.ocaml.org/doc/Install.html): + +```shell +opam repo add coq-released https://coq.inria.fr/opam/released +opam install coq-coq-art +``` + +To instead build and install manually, do: + +``` shell +git clone https://github.com/coq-community/coq-art +cd coq-art +make # or make -j +make install +``` + +After installation, the included modules are available under +the `coqart89` namespace. + + +## Documentation + +For more information, see the [book website][book-url] +and the [publisher's website][publisher-url]. + +The repository is structured as follows. + +### Book chapters + +1. [A Brief Presentation of Coq](ch1_overview) +2. [Gallina: Coq as a Programming Language](ch2_types_expressions) +3. [Propositions and Proofs](ch3_propositions_proofs) +4. [Dependent Product](ch4_dependent_product) +5. [Everyday Logic](ch5_everydays_logic) +6. [Inductive Data Structures](ch5_everydays_logic) +7. [Tactics and automation](ch5_everydays_logic) +8. [Inductive Predicates](ch8_inductive_predicates) +9. [Functions and their specification](ch9_function_specification) +10. [Extraction and imperative programming](ch10_extraction_and_imperative_programs) +11. [A Case Study: binary search trees](ch11_search_trees) +12. [The Module System](ch12_modules) +13. [Infinite Objects and Proofs](ch13_co_inductive_types) +14. [Foundations of Inductive Types](ch14_fundations_of_inductive_types) +15. [General Recursion](ch15_general_recursion) +16. [Proof by reflection](ch16_proof_by_reflection) + +### Additional material + +- [Tutorial on type classes](tutorial_type_classes) +- [Tutorial on inductive and coinductive types](tutorial_inductive_co_inductive_types) + +[book-url]: http://www.labri.fr/perso/casteran/CoqArt/ +[publisher-url]: https://www.springer.com/gp/book/9783540208549 diff --git a/coq-coq-art.opam b/coq-coq-art.opam new file mode 100644 index 0000000..d432ad4 --- /dev/null +++ b/coq-coq-art.opam @@ -0,0 +1,32 @@ +opam-version: "2.0" +maintainer: "palmskog@gmail.com" + +homepage: "https://github.com/coq-community/coq-art" +dev-repo: "git+https://github.com/coq-community/coq-art.git" +bug-reports: "https://github.com/coq-community/coq-art/issues" +license: "CECILL-B" + +synopsis: "Coq sources and exercises from the Coq'Art book" +description: """ +Coq'Art is the familiar name for the first book on the Coq proof assistant +and its underlying theory, the Calculus of Inductive Constructions. +This project contains the source of all examples and the solution to 170 +out of over 200 exercises from the book. +""" + +build: [make "-j%{jobs}%"] +install: [make "install"] +depends: [ + "ocaml" + "coq" {>= "8.9" & < "8.10~"} +] + +tags: [ + "category:Miscellaneous/Coq Use Examples" + "keyword:calculus of constructions" + "logpath:coqart89" +] +authors: [ + "Yves Bertot" + "Pierre Castéran" +] diff --git a/default.nix b/default.nix new file mode 100644 index 0000000..36a83e2 --- /dev/null +++ b/default.nix @@ -0,0 +1,25 @@ +{ pkgs ? (import {}), coq-version-or-url, shell ? false }: + +let + coq-version-parts = builtins.match "([0-9]+).([0-9]+)" coq-version-or-url; + coqPackages = + if coq-version-parts == null then + pkgs.mkCoqPackages (import (fetchTarball coq-version-or-url) {}) + else + pkgs."coqPackages_${builtins.concatStringsSep "_" coq-version-parts}"; +in + +with coqPackages; + +pkgs.stdenv.mkDerivation { + + name = "coq-art"; + + propagatedBuildInputs = [ + coq + ]; + + src = if shell then null else ./.; + + installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; +} diff --git a/meta.yml b/meta.yml new file mode 100644 index 0000000..7dbdc65 --- /dev/null +++ b/meta.yml @@ -0,0 +1,88 @@ +--- +fullname: Coq'Art +shortname: coq-art +organization: coq-community +community: true + +synopsis: Coq sources and exercises from the Coq'Art book + +description: | + Coq'Art is the familiar name for the first book on the Coq proof assistant + and its underlying theory, the Calculus of Inductive Constructions. + This project contains the source of all examples and the solution to 170 + out of over 200 exercises from the book. + +paper: + doi: 10.1007/978-3-662-07964-5 + +authors: +- name: Yves Bertot + initial: true +- name: Pierre Castéran + initial: true + +maintainers: +- name: Yves Bertot + nickname: ybertot +- name: Pierre Castéran + nickname: Casteran + +opam-file-maintainer: palmskog@gmail.com + +license: + fullname: CeCILL-B + identifier: CECILL-B + +supported_coq_versions: + text: 8.9 + opam: '{>= "8.9" & < "8.10~"}' + +tested_coq_nix_versions: +- version_or_url: 8.9 + +tested_coq_opam_versions: +- version: 8.9 + +namespace: coqart89 + +keywords: +- name: calculus of constructions + +categories: +- name: Miscellaneous/Coq Use Examples + +documentation: |- + ## Documentation + + For more information, see the [book website][book-url] + and the [publisher's website][publisher-url]. + + The repository is structured as follows. + + ### Book chapters + + 1. [A Brief Presentation of Coq](ch1_overview) + 2. [Gallina: Coq as a Programming Language](ch2_types_expressions) + 3. [Propositions and Proofs](ch3_propositions_proofs) + 4. [Dependent Product](ch4_dependent_product) + 5. [Everyday Logic](ch5_everydays_logic) + 6. [Inductive Data Structures](ch5_everydays_logic) + 7. [Tactics and automation](ch5_everydays_logic) + 8. [Inductive Predicates](ch8_inductive_predicates) + 9. [Functions and their specification](ch9_function_specification) + 10. [Extraction and imperative programming](ch10_extraction_and_imperative_programs) + 11. [A Case Study: binary search trees](ch11_search_trees) + 12. [The Module System](ch12_modules) + 13. [Infinite Objects and Proofs](ch13_co_inductive_types) + 14. [Foundations of Inductive Types](ch14_fundations_of_inductive_types) + 15. [General Recursion](ch15_general_recursion) + 16. [Proof by reflection](ch16_proof_by_reflection) + + ### Additional material + + - [Tutorial on type classes](tutorial_type_classes) + - [Tutorial on inductive and coinductive types](tutorial_inductive_co_inductive_types) + + [book-url]: http://www.labri.fr/perso/casteran/CoqArt/ + [publisher-url]: https://www.springer.com/gp/book/9783540208549 +--- From b007e569575092ab11049c8ef323026a355f1981 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 28 Jul 2019 16:46:06 -0500 Subject: [PATCH 3/4] license placeholder --- LICENSE | 1 + 1 file changed, 1 insertion(+) create mode 100644 LICENSE diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..d25fca4 --- /dev/null +++ b/LICENSE @@ -0,0 +1 @@ +All of the Coq'Art examples and solutions of the exercises are available under the CeCILL-B license. From 3679871d1d99815ad21c0a71d701ead01e6c752e Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 28 Jul 2019 16:48:12 -0500 Subject: [PATCH 4/4] add standard Makefile --- .gitignore | 3 +- Makefile | 808 +---------------------------------------------------- 2 files changed, 13 insertions(+), 798 deletions(-) diff --git a/.gitignore b/.gitignore index ddd306f..d7423c8 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ -Makefile.conf +Makefile.coq +Makefile.coq.conf execute_loops.ml execute_loops.mli insert-sort.ml diff --git a/Makefile b/Makefile index 3d05fd8..3e77020 100644 --- a/Makefile +++ b/Makefile @@ -1,802 +1,16 @@ -############################################################################### -## v # The Coq Proof Assistant ## -## /dev/null 2>/dev/null; echo $$?)) -STDTIME?=command time -f $(TIMEFMT) -else -ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=gtime -f $(TIMEFMT) -else -STDTIME?=command time -endif -endif -else -STDTIME?=command time -f $(TIMEFMT) -endif - -# Coq binaries -COQC ?= "$(COQBIN)coqc" -COQTOP ?= "$(COQBIN)coqtop" -COQCHK ?= "$(COQBIN)coqchk" -COQDEP ?= "$(COQBIN)coqdep" -COQDOC ?= "$(COQBIN)coqdoc" -COQMKFILE ?= "$(COQBIN)coq_makefile" - -# Timing scripts -COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" -BEFORE ?= -AFTER ?= - -# FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=camlp5.gramlib,unix,str - -# OCaml binaries -CAMLC ?= "$(OCAMLFIND)" ocamlc -c -CAMLOPTC ?= "$(OCAMLFIND)" opt -c -CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) -CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) -CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack - -# DESTDIR is prepended to all installation paths -DESTDIR ?= - -# Debug builds, typically -g to OCaml, -debug to Coq. -CAMLDEBUG ?= -COQDEBUG ?= - -# Extra packages to be linked in (as in findlib -package) -CAMLPKGS ?= - -# Option for making timing files -TIMING?= -# Option for changing sorting of timing output file -TIMING_SORT_BY ?= auto -# Output file names for timed builds -TIME_OF_BUILD_FILE ?= time-of-build.log -TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log -TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log -TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log -TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log -TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line - -########## End of parameters ################################################## -# What follows may be relevant to you only if you need to -# extend this Makefile. If so, look for 'Extension point' here and -# put in Makefile.local double colon rules accordingly. -# E.g. to perform some work after the all target completes you can write -# -# post-all:: -# echo "All done!" -# -# in Makefile.local -# -############################################################################### - - - - -# Flags ####################################################################### -# -# We define a bunch of variables combining the parameters. -# To add additional flags to coq, coqchk or coqdoc, set the -# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. -# To overwrite the default choice and set your own flags entirely, set the -# {COQ,COQCHK,COQDOC}FLAGS variable. - -SHOW := $(if $(VERBOSE),@true "",@echo "") -HIDE := $(if $(VERBOSE),,@) - -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - -OPT?= - -# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d -ifeq '$(OPT)' '-byte' -USEBYTE:=true -DYNOBJ:=.cma -DYNLIB:=.cma -else -USEBYTE:= -DYNOBJ:=.cmxs -DYNLIB:=.cmxs -endif - -# these variables are meant to be overriden if you want to add *extra* flags -COQEXTRAFLAGS?= -COQCHKEXTRAFLAGS?= -COQDOCEXTRAFLAGS?= - -# these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS) -COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) -COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) - -COQDOCLIBS?=$(COQLIBS_NOML) - -# The version of Coq being run and the version of coq_makefile that -# generated this makefile -COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) -COQMAKEFILE_VERSION:=8.9.1 - -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") - -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) - -# ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) - -# FIXME This should be generated by Coq -GRAMMARS:=grammar.cma -CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo - -CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) -ifeq (,$(CAMLLIB)) -PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") -else -PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' -endif - -ifneq (,$(TIMING)) -TIMING_ARG=-time -ifeq (after,$(TIMING)) -TIMING_EXT=after-timing -else -ifeq (before,$(TIMING)) -TIMING_EXT=before-timing -else -TIMING_EXT=timing -endif -endif -else -TIMING_ARG= -endif - -# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) -ifdef DSTROOT -DESTDIR := $(DSTROOT) -endif - -concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2)) - -COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) -COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) -COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) - -# Files ####################################################################### -# -# We here define a bunch of variables about the files being part of the -# Coq project in order to ease the writing of build target and build rules - -VDFILE := .coqdeps - -ALLSRCFILES := \ - $(ML4FILES) \ - $(MLFILES) \ - $(MLPACKFILES) \ - $(MLLIBFILES) \ - $(MLIFILES) - -# helpers -vo_to_obj = $(addsuffix .o,\ - $(filter-out Warning: Error:,\ - $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) -strip_dotslash = $(patsubst ./%,%,$(1)) -VO = vo - -VOFILES = $(VFILES:.v=.$(VO)) -GLOBFILES = $(VFILES:.v=.glob) -HTMLFILES = $(VFILES:.v=.html) -GHTMLFILES = $(VFILES:.v=.g.html) -BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) -TEXFILES = $(VFILES:.v=.tex) -GTEXFILES = $(VFILES:.v=.g.tex) -CMOFILES = \ - $(ML4FILES:.ml4=.cmo) \ - $(MLFILES:.ml=.cmo) \ - $(MLPACKFILES:.mlpack=.cmo) -CMXFILES = $(CMOFILES:.cmo=.cmx) -OFILES = $(CMXFILES:.cmx=.o) -CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) -CMXAFILES = $(CMAFILES:.cma=.cmxa) -CMIFILES = \ - $(CMOFILES:.cmo=.cmi) \ - $(MLIFILES:.mli=.cmi) -# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just -# a .ml4 file -CMXSFILES = \ - $(MLPACKFILES:.mlpack=.cmxs) \ - $(CMXAFILES:.cmxa=.cmxs) \ - $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs)) - -# files that are packed into a plugin (no extension) -PACKEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) -# files that are archived into a .cma (mllib) -LIBEDFILES = \ - $(call strip_dotslash, \ - $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib)))) -CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) -CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) -OBJFILES = $(call vo_to_obj,$(VOFILES)) -ALLNATIVEFILES = \ - $(OBJFILES:.o=.cmi) \ - $(OBJFILES:.o=.cmx) \ - $(OBJFILES:.o=.cmxs) -# trick: wildcard filters out non-existing files, so that `install` doesn't show -# warnings and `clean` doesn't pass to rm a list of files that is too long for -# the shell. -NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) -FILESTOINSTALL = \ - $(VOFILES) \ - $(VFILES) \ - $(GLOBFILES) \ - $(NATIVEFILES) \ - $(CMIFILESTOINSTALL) -BYTEFILESTOINSTALL = \ - $(CMOFILESTOINSTALL) \ - $(CMAFILES) -ifeq '$(HASNATDYNLINK)' 'true' -DO_NATDYNLINK = yes -FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) -else -DO_NATDYNLINK = -endif - -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE)) - -# Compilation targets ######################################################### - -all: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all -.PHONY: all - -all.timing.diff: - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all -.PHONY: all.timing.diff - -make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) -make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) -make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) - $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed -print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -ifeq (,$(BEFORE)) -print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' - $(HIDE)false -else -ifeq (,$(AFTER)) -print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' - $(HIDE)false -else -print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) -endif -endif -pretty-timed: - $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed -.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff - -# Extension points for actions to be performed before/after the all target -pre-all:: - @# Extension point - $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ - echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ - echo "W: while the current Coq version is $(COQ_VERSION)";\ - fi -.PHONY: pre-all - -post-all:: - @# Extension point -.PHONY: post-all - -real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) -.PHONY: real-all - -real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONY: real-all.timing.diff - -bytefiles: $(CMOFILES) $(CMAFILES) -.PHONY: bytefiles - -optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) -.PHONY: optfiles - -# FIXME, see Ralf's bugreport -quick: $(VOFILES:.vo=.vio) -.PHONY: quick - -vio2vo: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -.PHONY: vio2vo - -quick2vo: - $(HIDE)make -j $(J) quick - $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ - viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ - if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ - done); \ - echo "VIO2VO: $$VIOFILES"; \ - if [ -n "$$VIOFILES" ]; then \ - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ - fi -.PHONY: quick2vo - -checkproofs: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -.PHONY: checkproofs - -validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^ -.PHONY: validate - -only: $(TGTS) -.PHONY: only - -# Documentation targets ####################################################### - -html: $(GLOBFILES) $(VFILES) - $(SHOW)'COQDOC -d html $(GAL)' - $(HIDE)mkdir -p html - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) - -mlihtml: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -d $@' - $(HIDE)mkdir $@ || rm -rf $@/* - $(HIDE)$(CAMLDOC) -html \ - -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) - -all-mli.tex: $(MLIFILES:.mli=.cmi) - $(SHOW)'CAMLDOC -latex $@' - $(HIDE)$(CAMLDOC) -latex \ - -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) - -all.ps: $(VFILES) - $(SHOW)'COQDOC -ps $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` - -all.pdf: $(VFILES) - $(SHOW)'COQDOC -pdf $(GAL)' - $(HIDE)$(COQDOC) \ - -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` - -# FIXME: not quite right, since the output name is different -gallinahtml: GAL=-g -gallinahtml: html - -all-gal.ps: GAL=-g -all-gal.ps: all.ps - -all-gal.pdf: GAL=-g -all-gal.pdf: all.pdf - -# ? -beautify: $(BEAUTYFILES) - for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done - @echo 'Do not do "make clean" until you are sure that everything went well!' - @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: beautify - -# Installation targets ######################################################## -# -# There rules can be extended in Makefile.local -# Extensions can't assume when they run. - -install: - $(HIDE)for f in $(FILESTOINSTALL); do\ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ "$$?" != "0" -o -z "$$df" ]; then\ - echo SKIP "$$f" since it has no logical path;\ - else\ - install -d "$(COQLIBINSTALL)/$$df" &&\ - install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ - echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ - fi;\ - done - $(HIDE)$(MAKE) install-extra -f "$(SELF)" -install-extra:: - @# Extension point -.PHONY: install install-extra - -install-byte: - $(HIDE)for f in $(BYTEFILESTOINSTALL); do\ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ - if [ "$$?" != "0" -o -z "$$df" ]; then\ - echo SKIP "$$f" since it has no logical path;\ - else\ - install -d "$(COQLIBINSTALL)/$$df" &&\ - install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ - echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ - fi;\ - done - -install-doc:: html mlihtml - @# Extension point - $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(HIDE)for i in html/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done - $(HIDE)install -d \ - "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE)for i in mlihtml/*; do \ - dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ - install -m 0644 "$$i" "$$dest";\ - echo INSTALL "$$i" "$$dest";\ - done -.PHONY: install-doc - -uninstall:: - @# Extension point - $(HIDE)for f in $(FILESTOINSTALL); do \ - df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ - instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ - rm -f "$$instf" &&\ - echo RM "$$instf" &&\ - (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ - done -.PHONY: uninstall - -uninstall-doc:: - @# Extension point - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" - $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' - $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true -.PHONY: uninstall-doc - -# Cleaning #################################################################### -# -# There rules can be extended in Makefile.local -# Extensions can't assume when they run. - -clean:: - @# Extension point - $(SHOW)'CLEAN' - $(HIDE)rm -f $(CMOFILES) - $(HIDE)rm -f $(CMIFILES) - $(HIDE)rm -f $(CMAFILES) - $(HIDE)rm -f $(CMOFILES:.cmo=.cmx) - $(HIDE)rm -f $(CMXAFILES) - $(HIDE)rm -f $(CMXSFILES) - $(HIDE)rm -f $(CMOFILES:.cmo=.o) - $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) - $(HIDE)rm -f $(ALLDFILES) - $(HIDE)rm -f $(NATIVEFILES) - $(HIDE)find . -name .coq-native -type d -empty -delete - $(HIDE)rm -f $(VOFILES) - $(HIDE)rm -f $(VOFILES:.vo=.vio) - $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) - $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex - $(HIDE)rm -f $(VFILES:.v=.glob) - $(HIDE)rm -f $(VFILES:.v=.tex) - $(HIDE)rm -f $(VFILES:.v=.g.tex) - $(HIDE)rm -f pretty-timed-success.ok - $(HIDE)rm -rf html mlihtml -.PHONY: clean - -cleanall:: clean - @# Extension point - $(SHOW)'CLEAN *.aux *.timing' - $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) - $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) - $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) -.PHONY: cleanall - -archclean:: - @# Extension point - $(SHOW)'CLEAN *.cmx *.o' - $(HIDE)rm -f $(NATIVEFILES) - $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) -.PHONY: archclean - - -# Compilation rules ########################################################### - -$(MLIFILES:.mli=.cmi): %.cmi: %.mli - $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< - -$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 - $(SHOW)'CAMLC -pp -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $< - -$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 - $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< - -$(MLFILES:.ml=.cmo): %.cmo: %.ml - $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< - -$(MLFILES:.ml=.cmx): %.cmx: %.ml - $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< - - -$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ - -linkall -shared -o $@ $< - -$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ - -$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ - - -$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa - $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ - -shared -linkall -o $@ $< - -$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx - $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< - -$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack - $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack - $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ - -$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack - $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ - -# This rule is for _CoqProject with no .mllib nor .mlpack -$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx - $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ - -shared -o $@ $< - -ifneq (,$(TIMING)) -TIMING_EXTRA = > $<.$(TIMING_EXT) -else -TIMING_EXTRA = -endif - -$(VOFILES): %.vo: %.v - $(SHOW)COQC $< - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) - -# FIXME ?merge with .vo / .vio ? -$(GLOBFILES): %.glob: %.v - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -quick $< - $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - -$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $< - $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" - -$(BEAUTYFILES): %.v.beautified: %.v - $(SHOW)'BEAUTIFY $<' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< - -$(TEXFILES): %.tex: %.v - $(SHOW)'COQDOC -latex $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ - -$(GTEXFILES): %.g.tex: %.v - $(SHOW)'COQDOC -latex -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ - -$(HTMLFILES): %.html: %.v %.glob - $(SHOW)'COQDOC -html $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ - -$(GHTMLFILES): %.g.html: %.v %.glob - $(SHOW)'COQDOC -html -g $<' - $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ - -# Dependency files ############################################################ - -ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) -else - ifeq ($(MAKECMDGOALS),) - -include $(ALLDFILES) - endif -endif - -.SECONDARY: $(ALLDFILES) - -redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) - -$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 - $(SHOW)'CAMLDEP -pp $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml - $(SHOW)'CAMLDEP $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) - -$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) - -# If this makefile is created using a _CoqProject we have coqdep get -# options from it. This avoids argument length limits for pathological -# projects. Note that extra options might be on the command line. -VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) - -$(VDFILE).d: $(VFILES) - $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) - -# Misc ######################################################################## - -byte: - $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" -.PHONY: byte - -opt: - $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" -.PHONY: opt - -# This is deprecated. To extend this makefile use -# extension points and Makefile.local -printenv:: - $(warning printenv is deprecated) - $(warning write extensions in Makefile.local or include Makefile.conf) - @echo 'LOCAL = $(LOCAL)' - @echo 'COQLIB = $(COQLIB)' - @echo 'DOCDIR = $(DOCDIR)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP5O = $(CAMLP5O)' - @echo 'CAMLP5BIN = $(CAMLP5BIN)' - @echo 'CAMLP5LIB = $(CAMLP5LIB)' - @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' - @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' - @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' - @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' - @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'PP = $(PP)' - @echo 'COQFLAGS = $(COQFLAGS)' - @echo 'COQLIB = $(COQLIBS)' - @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' - @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' -.PHONY: printenv - -# Generate a .merlin file. If you need to append directives to this -# file you can extend the merlin-hook target in Makefile.local -.merlin: - $(SHOW)'FILL .merlin' - $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin - $(HIDE)echo 'B $(COQLIB)' >> .merlin - $(HIDE)echo 'S $(COQLIB)' >> .merlin - $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo 'B $(COQLIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ - echo 'S $(COQLIB)$(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) - $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) - $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" -.PHONY: merlin - -merlin-hook:: - @# Extension point -.PHONY: merlin-hook - -# prints all variables -debug: - $(foreach v,\ - $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ - $(.VARIABLES))),\ - $(info $(v) = $($(v)))) -.PHONY: debug - -.DEFAULT_GOAL := all +.PHONY: all clean