From 32d80150ff2e133281ef32b113939b063a97b749 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sat, 30 Mar 2024 00:03:58 -0700 Subject: [PATCH] initial commit --- .gitignore | 6 + Basics.v | 511 ++++++++++++++++++++++++++ Induction.v | 242 ++++++++++++ Makefile | 989 ++++++++++++++++++++++++++++++++++++++++++++++++++ Makefile.conf | 71 ++++ _CoqProject | 1 + 6 files changed, 1820 insertions(+) create mode 100644 .gitignore create mode 100644 Basics.v create mode 100644 Induction.v create mode 100644 Makefile create mode 100644 Makefile.conf create mode 100644 _CoqProject diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..da8f6cd --- /dev/null +++ b/.gitignore @@ -0,0 +1,6 @@ +*.glob +*.vo +*.vok +*.vos +.Makefile.d +*.aux diff --git a/Basics.v b/Basics.v new file mode 100644 index 0000000..7fcd1ef --- /dev/null +++ b/Basics.v @@ -0,0 +1,511 @@ +Inductive day : Type := +| monday +| tuesday +| wednesday +| thursday +| friday +| saturday +| sunday. + +Definition next_weekday (d : day) : day := + match d with + | monday => tuesday + | tuesday => wednesday + | wednesday => thursday + | thursday => friday + | friday => saturday + | saturday => sunday + | sunday => monday + end. + +Example test_next_weekday: + (next_weekday (next_weekday saturday)) = monday. +Proof. + simpl. + reflexivity. +Qed. + +Inductive bool : Type := +| true +| false. + +Definition negb (b : bool) : bool := + match b with + | true => false + | false => true + end. + +Definition andb (b1 : bool) (b2 : bool) : bool := + match b1 with + | true => b2 + | false => false + end. + +Definition orb (b1 : bool) (b2 : bool) : bool := + match b1 with + | true => true + | false => b2 + end. + +Example test_orb1: (orb true false) = true. +Proof. + simpl. + reflexivity. +Qed. + +Notation "x && y" := (andb x y). +Notation "x || y" := (orb x y). + +Example test_orb2: false || false || true = true. +Proof. + simpl. + reflexivity. +Qed. + +Definition nandb (b1: bool) (b2: bool) : bool := + negb (b1 && b2). + +Definition andb3 (b1 : bool) (b2 : bool) (b3 : bool) : bool := + b1 && b2 && b3. + +Inductive rgb : Type := +| red +| green +| blue. + +Inductive color : Type := +| black +| white +| primary (p : rgb). + +Definition monochrome (c : color) : bool := + match c with + | black => true + | white => true + | primary p => false + end. + +Definition isred (c : color) : bool := + match c with + | primary red => true + | _ => false + end. + +Module Playground. + Definition foo : rgb := blue. +End Playground. + +Module NatPlayground. + Inductive nat : Type := + | O + | S (n : nat). + + Definition pred (n : nat) : nat := + match n with + | O => O + | S n' => n' + end. + +End NatPlayground. + +Fixpoint even (n : nat) : bool := + match n with + | 0 => true + | 1 => false + | S (S n') => even n' + end. + +Definition odd (n: nat) : bool := + negb (even n). + +Example test_odd1 : odd 1 = true. +Proof. + simpl. + reflexivity. +Qed. + +Module NatPlayground2. + Fixpoint plus (n : nat) (m : nat) : nat := + match n with + | 0 => m + | S n' => S (plus n' m) + end. + + Compute (plus 3 2). + + Fixpoint mult (n m : nat) : nat := + match n with + | 0 => 0 + | S n' => plus m (mult n' m) + end. + + Compute (mult 2 4). + +End NatPlayground2. + +Fixpoint factorial (n : nat) : nat := + match n with + | 0 => 1 + | S n' => n * factorial n' + end. + +Fixpoint eqb (n m : nat) : bool := + match n, m with + | 0, 0 => true + | 0, S m' => false + | S n', 0 => false + | S n', S m' => eqb n' m' + end. + +Notation "x =? y" := (eqb x y) (at level 70) : nat_scope. + +Fixpoint leb (n m : nat) : bool := + match n, m with + | 0, _ => true + | S n', 0 => false + | S n', S m' => leb n' m' + end. + +Notation "x <=? y" := (leb x y) (at level 70) : nat_scope. + +Definition ltb (n m : nat) : bool := + negb (m <=? n). + +Notation "x + n + n = m + m. +Proof. + intros n m. + intros H. + rewrite H. + reflexivity. +Qed. + +Theorem plus_id_exercise : forall n m o : nat, + n = m -> m = o -> n + m = m + o. +Proof. + intros n m o. + intros H1 H2. + rewrite H1. + rewrite H2. + reflexivity. +Qed. + +Theorem plus_1_neq_0 : forall n : nat, + (n + 1) =? 0 = false. +Proof. + intros n. + destruct n as [| n'] eqn:E. + - reflexivity. + - reflexivity. +Qed. + +Theorem negb_involutive: forall b : bool, + negb (negb b) = b. +Proof. + intros b. + destruct b eqn:E. + - reflexivity. + - reflexivity. +Qed. + +Theorem andb_commutative : forall b c, b && c = c && b. +Proof. + intros b c. + destruct b eqn:Eb. + - destruct c eqn:Ec. + + reflexivity. + + reflexivity. + - destruct c eqn:Ec. + + reflexivity. + + reflexivity. +Qed. + +Theorem andb_true_elim2 : forall b c : bool, + b && c = true -> c = true. +Proof. + intros b c. + destruct b eqn:Eqb. + - simpl. + intros H. + apply H. + - destruct c eqn:Eqc. + + intros H. + reflexivity. + + intros H. + apply H. +Qed. + +Theorem zero_nbeq_plus_q : forall n : nat, + 0 =? (n + 1) = false. +Proof. + intros [|n]. + - reflexivity. + - reflexivity. +Qed. + +Theorem identity_fn_applied_twice : + forall (f : bool -> bool), + (forall (x : bool), f x = x) -> + forall (b : bool), f (f b) = b. +Proof. + intros f H b. + rewrite H. + rewrite H. + reflexivity. +Qed. + +Theorem negation_fn_applied_twice : + forall (f : bool -> bool), + (forall (x : bool), f x = negb x) -> + forall (b : bool), f (f b) = b. +Proof. + intros f H. + intros []. + - rewrite H. + rewrite H. + reflexivity. + - rewrite H. + rewrite H. + reflexivity. +Qed. + +Lemma true_and_b : forall b: bool, true && b = b. +Proof. + intros b. + reflexivity. +Qed. + +Lemma false_or_b : forall b: bool, false || b = b. +Proof. + intros b. + reflexivity. +Qed. + +Theorem andb_eq_orb : + forall (b c : bool), + (b && c = b || c) -> + b = c. +Proof. + intros [] c H. + - simpl in H. + rewrite H. + reflexivity. + - simpl in H. + rewrite H. + reflexivity. +Qed. + + + +Module LateDays. + Inductive letter : Type := + | A | B | C | D | F. + + Inductive modifier : Type := + | Plus | Natural | Minus. + + Inductive grade : Type := + Grade (l : letter) (m : modifier). + + Inductive comparison : Type := + | Eq + | Lt + | Gt. + + Definition letter_comparison (l1 l2 : letter) : comparison := + match l1, l2 with + | A, A => Eq + | A, _ => Gt + | B, A => Lt + | B, B => Eq + | B, _ => Gt + | C, (A | B) => Lt + | C, C => Eq + | C, _ => Gt + | D, (A | B | C) => Lt + | D, D => Eq + | D, _ => Gt + | F, F => Eq + | F, _ => Lt + end. + + Theorem letter_comparison_Eq : + forall l, letter_comparison l l = Eq. + Proof. + intros []. + - reflexivity. + - reflexivity. + - reflexivity. + - reflexivity. + - reflexivity. + Qed. + + Definition modifier_comparison (m1 m2 : modifier) : comparison := + match m1, m2 with + | Plus, Plus => Eq + | Plus, _ => Gt + | Natural, Plus => Lt + | Natural, Natural => Eq + | Natural, _ => Gt + | Minus, Minus => Eq + | Minus, _ => Lt + end. + + Definition grade_comparison (g1 g2: grade) : comparison := + match g1, g2 with + | Grade l1 m1, Grade l2 m2 => + match letter_comparison l1 l2, modifier_comparison m1 m2 with + | Lt, _ => Lt + | Gt, _ => Gt + | Eq, comp => comp + end + end. + + Definition lower_letter (l : letter) : letter := + match l with + | A => B + | B => C + | C => D + | D => F + | F => F + end. + + Theorem lower_letter_lowers: + forall (l : letter), + letter_comparison F l = Lt -> + letter_comparison (lower_letter l) l = Lt. + Proof. + intros [] H. + - reflexivity. + - reflexivity. + - reflexivity. + - reflexivity. + - apply H. + Qed. + + Definition lower_grade (g : grade) : grade := + match g with + | Grade l Plus => Grade l Natural + | Grade l Natural => Grade l Minus + | Grade l Minus => match l with + | F => Grade F Minus + | l' => Grade (lower_letter l') Plus + end + end. + + Theorem lower_grade_F_Minus : lower_grade (Grade F Minus) = Grade F Minus. + Proof. + reflexivity. + Qed. + + Lemma eq_letter_comp_modifier : + forall (g1 g2 : grade), + match g1, g2 with + Grade l1 m1, Grade l2 m2 => + letter_comparison l1 l2 = Eq -> + grade_comparison g1 g2 = modifier_comparison m1 m2 + end. + Proof. + intros [l1 m1] [l2 m2] H. + simpl. + rewrite H. + reflexivity. + Qed. + + Theorem lower_grade_lowers : + forall (g : grade), + grade_comparison (Grade F Minus) g = Lt -> + grade_comparison (lower_grade g) g = Lt. + Proof. + intros [l m] H. + destruct m eqn:Eqm. + - simpl. + rewrite letter_comparison_Eq. + reflexivity. + - simpl. + rewrite letter_comparison_Eq. + reflexivity. + - simpl. + destruct l eqn:Eql. + + reflexivity. + + reflexivity. + + reflexivity. + + reflexivity. + + rewrite H. + reflexivity. + Qed. + + Definition apply_late_policy (late_days : nat) (g : grade) : grade := + if late_days + apply_late_policy late_days g = g. + Proof. + intros. + rewrite apply_late_policy_unfold. + rewrite H. + reflexivity. + Qed. +End LateDays. + +Module Bin. + Inductive bin : Type := + | Z + | B0 (n : bin) + | B1 (n : bin). + + Fixpoint incr (m : bin) : bin := + match m with + | Z => B0 Z + | B0 b => B1 b + | B1 b => B0 (incr b) + end. + + Fixpoint bin_to_nat (m : bin) : nat := + match m with + | Z => O + | B0 b => 2 * bin_to_nat b + | B1 b => 1 + 2 * bin_to_nat b + end. +End Bin. diff --git a/Induction.v b/Induction.v new file mode 100644 index 0000000..b48faf2 --- /dev/null +++ b/Induction.v @@ -0,0 +1,242 @@ +From LF Require Export Basics. + +Theorem add_0_r : forall n : nat, + n + 0 = n. +Proof. + intros n. + induction n as [| n' IHn']. + - reflexivity. + - simpl. + rewrite IHn'. + reflexivity. +Qed. + +Theorem minus_n_n : forall n, + n - n = 0. +Proof. + intros. + induction n as [ | n' IHn']. + - reflexivity. + - simpl. + rewrite IHn'. + reflexivity. +Qed. + +Theorem mul_0_r : forall n : nat, + n * 0 = 0. +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - simpl. + rewrite IHn'. + reflexivity. +Qed. + +Theorem plus_n_Sm : forall n m : nat, + S (n + m) = n + (S m). +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - intros m. + simpl. + rewrite IHn'. + reflexivity. +Qed. + +Theorem add_comm : forall n m : nat, + n + m = m + n. +Proof. + induction n as [ | n' IHn']. + - intros m. + rewrite add_0_r. + reflexivity. + - intros m. + simpl. + rewrite plus_n_Sm. + rewrite IHn'. + simpl. + rewrite plus_n_Sm. + reflexivity. +Qed. + +Theorem sn_eq_sm_n_eq_m : forall n m : nat, + S n = S m -> n = m. +Proof. + intros n m H. + inversion H. + reflexivity. +Qed. + +Theorem n_eq_m_sn_eq_sm : forall n m : nat, + n = m -> S n = S m. +Proof. + intros n m H. + rewrite H. + reflexivity. +Qed. + +Theorem add_assoc : forall n m p : nat, + n + (m + p) = (n + m) + p. +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - simpl. + intros m p. + apply n_eq_m_sn_eq_sm. + rewrite IHn'. + reflexivity. +Qed. + +Fixpoint double (n : nat) := + match n with + | O => O + | S n' => S (S (double n')) + end. + +Lemma double_plus : forall n, double n = n + n. +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - simpl. + apply n_eq_m_sn_eq_sm. + rewrite IHn'. + apply plus_n_Sm. +Qed. + +Theorem eqb_refl : forall n : nat, + (n =? n) = true. +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - simpl. + rewrite IHn'. + reflexivity. +Qed. + +Theorem even_S : forall n : nat, + even (S n) = negb (even n). +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - rewrite IHn'. + rewrite negb_involutive. + reflexivity. +Qed. + +Theorem mult_0_plus' : forall n m : nat, + (n + 0 + 0) * m = n * m. +Proof. + intros n m. + assert (H : n + 0 + 0 = n). + - rewrite add_comm. + simpl. + rewrite add_comm. + reflexivity. + - rewrite H. + reflexivity. +Qed. + +Lemma n_zero_zero : forall n : nat, + n * 0 = 0. +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - simpl. + rewrite IHn'. + reflexivity. +Qed. + +Theorem add_shuffle3 : forall n m p : nat, + n + (m + p) = m + (n + p). +Proof. + intros n m p. + rewrite add_assoc. + assert (H: n + m = m + n). + { rewrite add_comm. reflexivity. } + rewrite H. + rewrite add_assoc. + reflexivity. +Qed. + +Lemma shuffle_4 : forall (a b c d : nat), + (a + b) + (c + d) = (a + c) + (b + d). +Proof. + intros a b c d. + assert (H: a + b + (c + d) = a + ((b + c) + d)). + { rewrite add_assoc. rewrite add_assoc. rewrite add_assoc. reflexivity. } + rewrite H. + assert (H1: b + c = c + b). + { rewrite add_comm. reflexivity. } + rewrite H1. + rewrite add_assoc. + rewrite add_assoc. + rewrite add_assoc. + reflexivity. +Qed. + +Theorem distributivity : forall (n m k : nat), + n * (m + k) = n * m + n * k. +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - intros m k. + simpl. + rewrite IHn'. + rewrite shuffle_4. + reflexivity. +Qed. + +Theorem n_one_n : forall n : nat, + n * 1 = n. +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - simpl. + rewrite IHn'. + reflexivity. +Qed. + +Theorem mul_comm : forall m n : nat, + m * n = n * m. +Proof. + induction n as [ | n' IHn']. + - rewrite n_zero_zero. + reflexivity. + - simpl. + assert (H: S n' = n' + 1). + { rewrite add_comm. reflexivity. } + rewrite H. + rewrite distributivity. + rewrite n_one_n. + rewrite IHn'. + rewrite add_comm. + reflexivity. +Qed. + +Theorem plus_leb_compact_l : forall n m p : nat, + n <=? m = true -> (p + n) <=? (p + m) = true. +Proof. + induction p as [ | p' IHp']. + - auto. + - intros H. + simpl. + apply IHp'. + rewrite H. + reflexivity. +Qed. + +Theorem leb_refl : forall n : nat, + (n <=? n) = true. +Proof. + induction n as [ | n' IHn']. + - reflexivity. + - simpl. + rewrite IHn'. + reflexivity. +Qed. + +Theorem zero_neqb_S : forall n : nat, + 0 =? (S n) = false. +Proof. + reflexivity. +Qed. diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..851734c --- /dev/null +++ b/Makefile @@ -0,0 +1,989 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # Copyright INRIA, CNRS and contributors ## +## /dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=command time +endif +endif +else +STDTIME?=command time -f $(TIMEFMT) +endif + +COQBIN?= +ifneq (,$(COQBIN)) +# add an ending / +COQBIN:=$(COQBIN)/ +endif + +# Coq binaries +COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" +COQCHK ?= "$(COQBIN)coqchk" +COQNATIVE ?= "$(COQBIN)coqnative" +COQDEP ?= "$(COQBIN)coqdep" +COQDOC ?= "$(COQBIN)coqdoc" +COQPP ?= "$(COQBIN)coqpp" +COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" + +# Timing scripts +COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py" +BEFORE ?= +AFTER ?= + +# OCaml binaries +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkall +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkall +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -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 ?= +FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS) + +# Option for making timing files +TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= +# Option for including the memory column(s) +TIMING_INCLUDE_MEM?= +# Option for sorting by the memory column +TIMING_SORT_BY_MEM?= +# 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 + +TGTS ?= + +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) +endif + +# Substitution of the path by appending $(DESTDIR) if needed. +# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. +windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) +destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) + +# Installation paths of libraries and documentation. +COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) +COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib) +COQPLUGININSTALL ?= $(call destination_path,$(COQCORELIB)/..) +COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? + +# findlib files installation +FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/" +FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/" + +# we need to move out of sight $(METAFILE) otherwise findlib thinks the +# package is already installed +findlib_install = \ + $(HIDE)if [ "$(METAFILE)" ]; then \ + $(FINDLIBPREINST) && \ + mv "$(METAFILE)" "$(METAFILE).skip" ; \ + "$(OCAMLFIND)" install $(2) $(FINDLIBDESTDIR) $(FINDLIBPACKAGE) $(1); \ + rc=$$?; \ + mv "$(METAFILE).skip" "$(METAFILE)"; \ + exit $$rc; \ + fi +findlib_remove = \ + $(HIDE)if [ ! -z "$(METAFILE)" ]; then\ + "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \ + fi + + +########## 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 overridden if you want to add *extra* flags +COQEXTRAFLAGS?= +COQCHKEXTRAFLAGS?= +COQDOCEXTRAFLAGS?= + +# Find the last argument of the form "-native-compiler FLAG" +COQUSERNATIVEFLAG:=$(strip \ +$(subst -native-compiler-,,\ +$(lastword \ +$(filter -native-compiler-%,\ +$(subst -native-compiler ,-native-compiler-,\ +$(strip $(COQEXTRAFLAGS))))))) + +COQFILTEREDEXTRAFLAGS:=$(strip \ +$(filter-out -native-compiler-%,\ +$(subst -native-compiler ,-native-compiler-,\ +$(strip $(COQEXTRAFLAGS))))) + +COQACTUALNATIVEFLAG:=$(lastword $(COQMF_COQ_NATIVE_COMPILER_DEFAULT) $(COQMF_COQPROJECTNATIVEFLAG) $(COQUSERNATIVEFLAG)) + +ifeq '$(COQACTUALNATIVEFLAG)' 'yes' + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" + COQDONATIVE="yes" +else +ifeq '$(COQACTUALNATIVEFLAG)' 'ondemand' + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" + COQDONATIVE="no" +else + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "no" + COQDONATIVE="no" +endif +endif + +# these flags do NOT contain the libraries, to make them easier to overwrite +COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG) +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.18.0 + +# COQ_SRC_SUBDIRS is for user-overriding, usually to add +# `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for +# Coq's own core libraries, which should be replaced by ocamlfind +# options at some point. +COQ_SRC_SUBDIRS?= +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") + +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) + +ifneq (,$(TIMING)) + ifeq (after,$(TIMING)) + TIMING_EXT=after-timing + else + ifeq (before,$(TIMING)) + TIMING_EXT=before-timing + else + TIMING_EXT=timing + endif + endif + TIMING_ARG=-time-file $<.$(TIMING_EXT) +else + TIMING_ARG= +endif + +# 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 := .Makefile.d + +ALLSRCFILES := \ + $(MLGFILES) \ + $(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)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + +VO = vo +VOS = vos + +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 = \ + $(MLGFILES:.mlg=.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 .mlg file +CMXSFILES = \ + $(MLPACKFILES:.mlpack=.cmxs) \ + $(CMXAFILES:.cmxa=.cmxs) \ + $(if $(MLPACKFILES)$(CMXAFILES),,\ + $(MLGFILES:.mlg=.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)),$(call with_undef,$(lib)))) +# files that are archived into a .cma (mllib) +LIBEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(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) +FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE))) + +# 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) \ + $(CMXSFILES) # to be removed when we remove legacy loading +FINDLIBFILESTOINSTALL = \ + $(CMIFILESTOINSTALL) +ifeq '$(HASNATDYNLINK)' 'true' +DO_NATDYNLINK = yes +FINDLIBFILESTOINSTALL += $(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 + +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + +ifeq (0,$(TIMING_INCLUDE_MEM)) +TIMING_INCLUDE_MEM_ARG := --no-include-mem +else +TIMING_INCLUDE_MEM_ARG := +endif + +ifeq (1,$(TIMING_SORT_BY_MEM)) +TIMING_SORT_BY_MEM_ARG := --sort-by-mem +else +TIMING_SORT_BY_MEM_ARG := +endif + +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) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(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) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(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) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(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 is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") +.PHONY: quick + +vio2vo: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ + -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +.PHONY: vio2vo + +# quick2vo is undocumented +quick2vo: + $(HIDE)make -j $(J) vio + $(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 + +vos: $(VOFILES:%.vo=%.vos) +.PHONY: vos + +vok: $(VOFILES:%.vo=%.vok) +.PHONY: vok + +validate: $(VOFILES) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ +.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) $(FINDLIBPKGS) + +all-mli.tex: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) + +all.ps: $(VFILES) + $(SHOW)'COQDOC -ps $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(VFILES)` + +all.pdf: $(VFILES) + $(SHOW)'COQDOC -pdf $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(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. + +# We use $(file) to avoid generating a very long command string to pass to the shell +# (cf https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Strange.20command.20length.20limit.20on.20Linux) +# However Apple ships old make which doesn't have $(file) so we need a fallback +$(file >.hasfile,1) +HASFILE:=$(shell if [ -e .hasfile ]; then echo 1; rm .hasfile; fi) + +MKFILESTOINSTALL= $(if $(HASFILE),$(file >.filestoinstall,$(FILESTOINSTALL)),\ + $(shell rm -f .filestoinstall) \ + $(foreach x,$(FILESTOINSTALL),$(shell printf '%s\n' "$x" >> .filestoinstall))) + +# findlib needs the package to not be installed, so we remove it before +# installing it (see the call to findlib_remove) +install: META + @$(MKFILESTOINSTALL) + $(HIDE)code=0; for f in $$(cat .filestoinstall); do\ + if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ + done; exit $$code + $(HIDE)for f in $$(cat .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 + $(call findlib_remove) + $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) + $(HIDE)$(MAKE) install-extra -f "$(SELF)" + @rm -f .filestoinstall +install-extra:: + @# Extension point +.PHONY: install install-extra + +META: $(METAFILE) + $(HIDE)if [ "$(METAFILE)" ]; then \ + cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ + fi + +install-byte: + $(call findlib_install, $(CMAFILES) $(CMOFILESTOINSTALL), -add) + +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 + @$(MKFILESTOINSTALL) + $(call findlib_remove) + $(HIDE)for f in $$(cat .filestoinstall); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" ;\ + done + $(HIDE)for f in $$(cat .filestoinstall); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ + (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ + done + @rm -f .filestoinstall + +.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 $(CMXFILES) + $(HIDE)rm -f $(CMXAFILES) + $(HIDE)rm -f $(CMXSFILES) + $(HIDE)rm -f $(OFILES) + $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(MLGFILES:.mlg=.ml) + $(HIDE)rm -f $(CMXFILES:.cmx=.cmt) + $(HIDE)rm -f $(MLIFILES:.mli=.cmti) + $(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 $(VOFILES:.vo=.vos) + $(HIDE)rm -f $(VOFILES:.vo=.vok) + $(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 -f META + $(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) + $(HIDE)rm -f .lia.cache .nia.cache +.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)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< + +$(MLGFILES:.mlg=.ml): %.ml: %.mlg + $(SHOW)'COQPP $<' + $(HIDE)$(COQPP) $< + +# Stupid hack around a deficient syntax: we cannot concatenate two expansions +$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml + $(SHOW)'CAMLC -c $<' + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< + +# Same hack +$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml + $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' + $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $(FOR_PACK) $< + + +$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -g -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -g -o $@ $< + +$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + +$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + + +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -g -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -g -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< + +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack + $(SHOW)'CAMLC -pack -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack + $(SHOW)'CAMLOPT -pack -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -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) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx + $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -g -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -g -o $@ $< + +# can't make +# https://www.gnu.org/software/make/manual/make.html#Static-Pattern +# work with multiple target rules +# so use eval in a loop instead +# with grouped targets https://www.gnu.org/software/make/manual/make.html#Multiple-Targets +# if available (GNU Make >= 4.3) +ifneq (,$(filter grouped-target,$(.FEATURES))) +define globvorule= + +# take care to $$ variables using $< etc + $(1).vo $(1).glob &: $(1).v | $(VDFILE) + $(SHOW)COQC $(1).v + $(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $$(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v +ifeq ($(COQDONATIVE), "yes") + $(SHOW)COQNATIVE $(1).vo + $(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo +endif + +endef +else + +$(VOFILES): %.vo: %.v | $(VDFILE) + $(SHOW)COQC $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< +ifeq ($(COQDONATIVE), "yes") + $(SHOW)COQNATIVE $@ + $(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@ +endif + +# this is broken :( todo fix if we ever find a solution that doesn't need grouped targets +$(GLOBFILES): %.glob: %.v + $(SHOW)'COQC $< (for .glob)' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +endif + +$(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile)))) + +$(VFILES:.v=.vio): %.vio: %.v + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vos): %.vos: %.v + $(SHOW)COQC -vos $< + $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vok): %.vok: %.v + $(SHOW)COQC -vok $< + $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing + $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing + $(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 ############################################################ + +ifndef MAKECMDGOALS + -include $(ALLDFILES) +else + 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) + endif +endif + +.SECONDARY: $(ALLDFILES) + +redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) + +GENMLFILES:=$(MLGFILES:.mlg=.ml) +$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) + +$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(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): _CoqProject $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -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 'COQLIB = $(COQLIB)' + @echo 'COQCORELIB = $(COQCORELIB)' + @echo 'DOCDIR = $(DOCDIR)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' + @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' + @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' + @echo 'COQCORE_SRC_SUBDIRS = $(COQCORE_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 $(COQCORELIB)' >> .merlin + $(HIDE)echo 'S $(COQCORELIB)' >> .merlin + $(HIDE)$(foreach d,$(COQCORE_SRC_SUBDIRS), \ + echo 'B $(COQCORELIB)$(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 + +# Users can create Makefile.local-late to hook into double-colon rules +# or add other needed Makefile code, using defined +# variables if necessary. +-include Makefile.local-late + +# Local Variables: +# mode: makefile-gmake +# End: diff --git a/Makefile.conf b/Makefile.conf new file mode 100644 index 0000000..9015f05 --- /dev/null +++ b/Makefile.conf @@ -0,0 +1,71 @@ +# This configuration file was generated by running: +# coq_makefile -f _CoqProject Basics.v -o Makefile + +COQBIN?= +ifneq (,$(COQBIN)) +# add an ending / +COQBIN:=$(COQBIN)/ +endif +COQMKFILE ?= "$(COQBIN)coq_makefile" + +############################################################################### +# # +# Project files. # +# # +############################################################################### + +COQMF_CMDLINE_VFILES := Basics.v +COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES)) +COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES)) +COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES)) +COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES)) +COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES)) +COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES)) +COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES)) +COQMF_METAFILE = + +############################################################################### +# # +# Path directives (-I, -R, -Q). # +# # +############################################################################### + +COQMF_OCAMLLIBS = +COQMF_SRC_SUBDIRS = +COQMF_COQLIBS = -Q . LF +COQMF_COQLIBS_NOML = -Q . LF +COQMF_CMDLINE_COQLIBS = + +############################################################################### +# # +# Coq configuration. # +# # +############################################################################### + +COQMF_COQLIB=/usr/lib64/ocaml/coq/ +COQMF_COQCORELIB=/usr/lib64/ocaml/coq/../coq-core/ +COQMF_DOCDIR=/usr/share/doc/coq/ +COQMF_OCAMLFIND=/usr/bin/ocamlfind +COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 +COQMF_WARN=-warn-error +a-3 +COQMF_HASNATDYNLINK=true +COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax +COQMF_COQ_NATIVE_COMPILER_DEFAULT=no +COQMF_WINDRIVE= + +############################################################################### +# # +# Native compiler. # +# # +############################################################################### + +COQMF_COQPROJECTNATIVEFLAG = + +############################################################################### +# # +# Extra variables. # +# # +############################################################################### + +COQMF_OTHERFLAGS = +COQMF_INSTALLCOQDOCROOT = LF diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..36aea0f --- /dev/null +++ b/_CoqProject @@ -0,0 +1 @@ +-Q . LF