diff --git a/coq/Arbiter.v b/coq/Arbiter.v
new file mode 100644
index 0000000000000000000000000000000000000000..5a7c7bb9c31c037aa91d111a14333499d5c1a004
--- /dev/null
+++ b/coq/Arbiter.v
@@ -0,0 +1,25 @@
+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype.
+From sdram Require Export Trace.
+
+Section Arbiter.
+ Context {BANK_CFG : Bank_configuration}.
+
+ Definition Match (req : Request_t) (cmd : Command_t) : bool :=
+ match req.(Kind), cmd.(CKind) with
+ | RD, CRD
+ | WR, CWR => (cmd.(Request) == req)
+ | _, _ => false
+ end.
+
+ Class Arbiter_t := mkArbiter
+ {
+ Input : Requests_t;
+
+ Arbitrate : Trace_t;
+
+ (* All Requests must handled *)
+ Req_handled : forall req, exists cmd, req \in Requests -> cmd \in Arbitrate.(Commands) ->
+ Match req cmd
+ }.
+End Arbiter.
diff --git a/coq/Bank.v b/coq/Bank.v
new file mode 100644
index 0000000000000000000000000000000000000000..728cbdf01d58b591a44040ac47408e8da768a9ed
--- /dev/null
+++ b/coq/Bank.v
@@ -0,0 +1,45 @@
+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Export ssreflect ssrnat ssrbool seq.
+
+
+Definition Bank_number_t := {B : nat | B <> 0}.
+Definition Timing_parameter_t := {T : nat | T <> 0}.
+
+Class Bank_configuration :=
+{
+ BANKS : Bank_number_t;
+
+ T_RC : Timing_parameter_t (* ACT to ACT delay intra-bank *)
+}.
+
+Section Banks.
+ Context {BANK_CFG : Bank_configuration}.
+
+ Definition BANKS_NAT := proj1_sig BANKS.
+ Definition T_RC_NAT := proj1_sig T_RC.
+
+ Definition Bank_t := { a : nat | a < BANKS_NAT }.
+
+ Program Definition Nat_to_bank a : Bank_t :=
+ match a < BANKS_NAT with
+ | true => (exist _ a _)
+ | false => (exist _ (BANKS_NAT - 1) _)
+ end.
+ Next Obligation.
+ unfold BANKS_NAT in *.
+ destruct BANKS. simpl in *.
+ apply PeanoNat.Nat.lt_pred_l in n as H. move : H => /ltP H. by rewrite subn1.
+ Qed.
+
+ Definition Bank_to_nat (a : Bank_t) : nat :=
+ proj1_sig a.
+
+ Notation "'#B' b" := (Nat_to_bank b) (only parsing, at level 0).
+ Notation "'#B' b" := ((exist _ b _) Bank_t) (only printing, at level 0).
+
+ Definition Banks_t := seq Bank_t.
+
+ Definition All_banks : Banks_t :=
+ map Nat_to_bank (iota 0 BANKS_NAT).
+End Banks.
+
diff --git a/coq/Commands.v b/coq/Commands.v
new file mode 100644
index 0000000000000000000000000000000000000000..c124f1a260e91627933a22eb3ff31cae30315fef
--- /dev/null
+++ b/coq/Commands.v
@@ -0,0 +1,84 @@
+Set Warnings "-notation-overridden,-parsing".
+From sdram Require Export Requests.
+
+Section Commands.
+ Context {BANK_CFG : Bank_configuration}.
+
+ Inductive Command_kind_t : Set :=
+ ACT |
+ PRE |
+ CRD |
+ CWR.
+
+ Local Definition Command_kind_eqdef (a b : Command_kind_t) :=
+ match a, b with
+ | ACT, ACT
+ | PRE, PRE
+ | CRD, CRD
+ | CWR, CWR => true
+ | _, _ => false
+ end.
+
+ Lemma Command_kind_eqn : Equality.axiom Command_kind_eqdef.
+ Proof.
+ unfold Equality.axiom. intros.
+ destruct (Command_kind_eqdef x y) eqn:H; unfold Command_kind_eqdef in *.
+ apply ReflectT. destruct x, y; inversion H; auto.
+ apply ReflectF; destruct x, y; inversion H; unfold not; intros; inversion H0.
+ Qed.
+
+ Canonical Command_kind_eqMixin := EqMixin Command_kind_eqn.
+ Canonical Command_kind_eqType := Eval hnf in EqType Command_kind_t Command_kind_eqMixin.
+
+ Record Command_t : Set := mkCmd
+ {
+ CDate : nat;
+ CKind : Command_kind_t;
+ Request : Request_t
+ }.
+
+ Local Definition Command_eqdef (a b : Command_t) :=
+ (a.(CDate) == b.(CDate)) &&
+ (a.(Request) == b.(Request)) &&
+ (a.(CKind) == b.(CKind)).
+
+ Lemma Command_eqn : Equality.axiom Command_eqdef.
+ Proof.
+ unfold Equality.axiom. intros. destruct Command_eqdef eqn:H; unfold Command_eqdef in *.
+ {
+ apply ReflectT.
+ move: H => /andP [/andP [/eqP CD /eqP R /eqP C]].
+ destruct x,y. simpl in *. subst. auto.
+ }
+ apply ReflectF. unfold not in *. intro BUG.
+ apply negbT in H; rewrite negb_and in H.
+ destruct x, y.
+ rewrite negb_and in H.
+ move: H => /orP [H | /eqP CK].
+ move: H => /orP [H | /eqP R].
+ move: H => /eqP CD.
+ by apply CD; inversion BUG.
+ by apply R; inversion BUG.
+ by apply CK; inversion BUG.
+ Qed.
+
+ Canonical Command_eqMixin := EqMixin Command_eqn.
+ Canonical Command_eqType := Eval hnf in EqType Command_t Command_eqMixin.
+
+ Definition Kind_of_req req :=
+ match req.(Kind) with
+ | RD => CRD
+ | WR => CWR
+ end.
+
+ Definition PRE_of_req req t :=
+ mkCmd t PRE req.
+
+ Definition ACT_of_req req t :=
+ mkCmd t ACT req.
+
+ Definition Cmd_of_req req t :=
+ mkCmd t (Kind_of_req req) req.
+
+ Definition Commands_t := seq Command_t.
+End Commands.
diff --git a/coq/FIFO.v b/coq/FIFO.v
new file mode 100644
index 0000000000000000000000000000000000000000..65328890e21145c48f70e949a79a6e9b45b0dd0a
--- /dev/null
+++ b/coq/FIFO.v
@@ -0,0 +1,73 @@
+Set Warnings "-notation-overridden,-parsing".
+From sdram Require Import Arbiter.
+
+Section FIFO.
+ Context {BANK_CFG : Bank_configuration}.
+ Context {Input : Requests_t}.
+
+ Local Record FIFO_state_t := mkFIFO
+ {
+ Cmds : Commands_t;
+ Time : nat;
+ }.
+
+ Definition FIFO_wait := T_RC.
+
+ Local Program Definition FIFO_req req State : FIFO_state_t :=
+ let PRE_date := State.(Time) + 1 in
+ let ACT_date := State.(Time) + 2 in
+ let CMD_date := State.(Time) + 3 in
+ let PRE := PRE_of_req req PRE_date in
+ let ACT := ACT_of_req req ACT_date in
+ let CMD := Cmd_of_req req CMD_date in
+ let Cmds := PRE::ACT::CMD::State.(Cmds) in
+ mkFIFO Cmds (State.(Time) + FIFO_wait).
+
+ Local Fixpoint FIFO_trace Reqs State : FIFO_state_t :=
+ match Reqs with
+ | [::] => State
+ | req::Reqs' => FIFO_req req (FIFO_trace Reqs' State)
+ end.
+
+ Lemma FIFO_trace_time_monotone Reqs State:
+ State.(Time) <= (FIFO_trace Reqs State).(Time).
+ Proof.
+ induction Reqs.
+ auto.
+ {
+ simpl. destruct FIFO_wait. simpl.
+ specialize (leq_addr x (Time (FIFO_trace Reqs State))) as H.
+ specialize leq_trans with (n := Time (FIFO_trace Reqs State)) (m := Time State) (p := Time (FIFO_trace Reqs State) + x) as H1.
+ apply H1 in IHReqs; auto.
+ }
+ Qed.
+
+ Program Definition FIFO_arbitrate :=
+ let State := FIFO_trace Requests (mkFIFO [::] 0) in
+ mkTrace State.(Cmds) State.(Time) _ _ _.
+ Admit Obligations.
+
+ Program Instance FIFO_arbiter : Arbiter_t :=
+ mkArbiter Input FIFO_arbitrate _.
+ Admit Obligations.
+End FIFO.
+
+Section Test.
+ Program Instance BANK_CFG : Bank_configuration :=
+ {
+ BANKS := 1;
+ T_RC := 2;
+ }.
+
+ Program Definition Req1 := mkReq 3 RD 0.
+ Program Definition Req2 := mkReq 4 RD 0.
+
+ Program Instance Input : Requests_t := mkReqs [:: Req1; Req2] _ _ _.
+ Admit Obligations.
+
+ Program Instance My_arbiter : Arbiter_t :=
+ mkArbiter Input FIFO_arbitrate _.
+ Admit Obligations.
+
+ Compute Arbitrate.(Commands).
+End Test.
diff --git a/coq/Requests.v b/coq/Requests.v
new file mode 100644
index 0000000000000000000000000000000000000000..9762b705617d03077a8537fb72344af51588c44f
--- /dev/null
+++ b/coq/Requests.v
@@ -0,0 +1,98 @@
+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Export ssreflect eqtype.
+From sdram Require Export Bank Util.
+
+Section Requests.
+ Context {BANK_CFG : Bank_configuration}.
+
+ Inductive Request_kind_t : Set :=
+ RD |
+ WR.
+
+ Local Definition Request_kind_eqdef (a b : Request_kind_t) :=
+ match a, b with
+ | RD, RD
+ | WR, WR => true
+ | _, _ => false
+ end.
+
+ Lemma Request_kind_eqn : Equality.axiom Request_kind_eqdef.
+ Proof.
+ unfold Equality.axiom. intros.
+ destruct (Request_kind_eqdef x y) eqn:H; unfold Request_kind_eqdef in *.
+ apply ReflectT. destruct x, y; inversion H; auto.
+ apply ReflectF; destruct x, y; inversion H; unfold not; intros; inversion H0.
+ Qed.
+
+ Canonical Request_kind_eqMixin := EqMixin Request_kind_eqn.
+ Canonical Request_kind_eqType:= Eval hnf in EqType Request_kind_t Request_kind_eqMixin.
+
+ Record Request_t : Set := mkReq
+ {
+ Date : nat;
+ Kind : Request_kind_t;
+ Bank : Bank_t;
+ }.
+
+ Notation "'*R' b '@' id '->' cd" := (mkReq id (Some cd) true (exist _ b _)) (only printing, at level 0).
+ Notation "'*W' b '@' id '->' cd" := (mkReq id (Some cd) false (exist _ b _)) (only printing, at level 0).
+ Notation "'*R' b '@' id" := (mkReq id None true (exist _ b _)) (only printing, at level 0).
+ Notation "'*W' b '@' id" := (mkReq id None false (exist _ b _)) (only printing, at level 0).
+
+ Local Definition Request_eqdef (a b : Request_t) :=
+ (a.(Date) == b.(Date)) &&
+ (a.(Kind) == b.(Kind)) &&
+ (a.(Bank) == b.(Bank)).
+
+ Lemma Request_eqn : Equality.axiom Request_eqdef.
+ Proof.
+ unfold Equality.axiom. intros. destruct Request_eqdef eqn:H.
+ {
+ apply ReflectT. unfold Request_eqdef in *.
+ move: H => /andP [/andP [/eqP ID /eqP RD /eqP B]].
+ destruct x,y; simpl in *. subst. auto.
+ }
+ apply ReflectF. unfold Request_eqdef, not in *.
+ intro BUG.
+ apply negbT in H; rewrite negb_and in H.
+ destruct x, y.
+ rewrite negb_and in H.
+ move: H => /orP [H | /eqP B].
+ move: H => /orP [H | /eqP RD].
+ move: H => /eqP ID.
+ by apply ID; inversion BUG.
+ by apply RD; inversion BUG.
+ by apply B; inversion BUG.
+ Qed.
+
+ Canonical Request_eqMixin := EqMixin Request_eqn.
+ Canonical Request_eqType := Eval hnf in EqType Request_t Request_eqMixin.
+
+ Local Fixpoint sorted_ (Reqs : seq Request_t) a :=
+ match Reqs with
+ | [::] => true
+ | b::Reqs' => (a.(Date) <= b.(Date)) &&
+ sorted_ Reqs' b
+ end.
+
+ Local Definition sorted (Reqs : seq Request_t) :=
+ match Reqs with
+ | [::] => true
+ | a::Reqs' => sorted_ Reqs' a
+ end.
+
+ Class Requests_t := mkReqs
+ {
+ Requests : seq Request_t;
+
+ (* All Requests must be uniq *)
+ Reqs_uniq : uniq Requests;
+
+ (* Requests are sorted by date. *)
+ Reqs_sorted : sorted Requests;
+
+ (* A requestor may only issue a single request to a bank at a time *)
+ Reqs_issue : forall a b, a \in Requests -> b \in Requests -> a != b ->
+ a.(Date) == b.(Date) -> a.(Bank) != b.(Bank);
+ }.
+End Requests.
diff --git a/coq/Trace.v b/coq/Trace.v
new file mode 100644
index 0000000000000000000000000000000000000000..e4fe177994588f218c445f81b3f3761104074412
--- /dev/null
+++ b/coq/Trace.v
@@ -0,0 +1,41 @@
+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Import ssreflect ssrnat ssrbool seq eqtype.
+From sdram Require Export Commands Bank.
+
+Section Trace.
+ Context {BANK_CFG : Bank_configuration}.
+
+ Definition isACT (cmd : Command_t) :=
+ cmd.(CKind) == ACT.
+
+ Definition Same_Bank (a b : Command_t) :=
+ a.(Request).(Bank) == b.(Request).(Bank).
+
+ Definition ACT_to_ACT (a b : Command_t) :=
+ isACT a && isACT b.
+
+ Definition Before (a b : Command_t) :=
+ a.(CDate) < b.(CDate).
+
+ Definition Apart (a b : Command_t) t :=
+ a.(CDate) + t < b.(CDate).
+
+ Record Trace_t := mkTrace
+ {
+ Commands : Commands_t;
+ Time : nat;
+
+ (* All commands must be uniq *)
+ Cmds_uniq : uniq Commands;
+
+ (* All commands have to occur before the current time instant *)
+ Cmds_time_ok : forall cmd, cmd \in Commands -> cmd.(CDate) <= Time;
+
+ (* Ensure that the time between two ACT commands respects T_RC *)
+ Cmds_T_RC_ok : forall a b, a \in Commands -> b \in Commands ->
+ ACT_to_ACT a b -> Same_Bank a b -> Before a b ->
+ Apart a b T_RC_NAT;
+ }.
+
+ Program Definition Trace_empty := mkTrace [::] 0 _ _ _.
+End Trace.
diff --git a/coq/Util.v b/coq/Util.v
new file mode 100644
index 0000000000000000000000000000000000000000..e0eba38b23bd33345c4db11795b85bc25b196968
--- /dev/null
+++ b/coq/Util.v
@@ -0,0 +1,56 @@
+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Import ssreflect ssrnat ssrbool seq eqtype.
+
+Lemma all_filter [T : eqType] a (p : pred T) S:
+ all a S -> all a [seq x <- S | p x].
+Proof.
+ intros.
+ induction S.
+ auto.
+ simpl in *.
+ destruct (p a0).
+ simpl. apply /andP.
+ split.
+ move : H => /andP /proj1 H. auto.
+ move : H => /andP /proj2 H. apply IHS in H. auto.
+ move : H => /andP /proj2 H. apply IHS in H. auto.
+Qed.
+
+(* TODO replace by generic definition *)
+Definition pred2_t (T : eqType) := T -> T -> bool.
+
+Definition all_pred2 [T : eqType] (p : pred2_t T) S x :=
+ all (p x) S.
+
+Lemma all_pred2_filter [T : eqType] (p2 : pred2_t T) (p : pred T) S (x : T):
+ all_pred2 p2 S x -> all_pred2 p2 [seq y <- S | p y] x.
+Proof.
+ unfold pred2_t.
+ intros.
+ by apply all_filter.
+Qed.
+
+Fixpoint all_pred2_recursive [T : eqType] (p2 : pred2_t T) S :=
+ match S with
+ | [::] => true
+ | x::S' => all_pred2 p2 S' x &&
+ all_pred2_recursive p2 S'
+ end.
+
+Lemma all_pred2_recursive_filter [T : eqType] (p2 : pred2_t T) (p : pred T) S:
+ all_pred2_recursive p2 S -> all_pred2_recursive p2 [seq x <- S | p x].
+Proof.
+ induction S; intros; auto.
+ simpl in *. move : H => /andP H.
+ destruct (p a); simpl.
+ apply /andP. split.
+ apply proj1 in H. by apply all_filter.
+ apply proj2 in H. by apply IHS in H.
+ apply proj2 in H. by apply IHS in H.
+Qed.
+
+(* Lemma filter_forall_pred [T : eqType] S (p : pred T): forall z , z \in [seq y <- S | p y ] -> p z.
+ intros.
+ rewrite (mem_filter p z S) in H. by move : H => /andP /proj1.
+Qed.
+ *)
diff --git a/coq/makefile b/coq/makefile
new file mode 100644
index 0000000000000000000000000000000000000000..4028ff0576b140d05de44027925e08eef2b27d0c
--- /dev/null
+++ b/coq/makefile
@@ -0,0 +1,870 @@
+##########################################################################
+## # The Coq Proof Assistant / The Coq Development Team ##
+## v # Copyright INRIA, CNRS and contributors ##
+## <O___,, # (see version control and CREDITS file for authors & dates) ##
+## \VV/ ###############################################################
+## // # This file is distributed under the terms of the ##
+## # GNU Lesser General Public License Version 2.1 ##
+## # (see LICENSE file for the text of the license) ##
+##########################################################################
+## GNUMakefile for Coq 8.13.1
+
+# For debugging purposes (must stay here, don't move below)
+INITIAL_VARS := $(.VARIABLES)
+# To implement recursion we save the name of the main Makefile
+SELF := $(lastword $(MAKEFILE_LIST))
+PARENT := $(firstword $(MAKEFILE_LIST))
+
+# This file is generated by coq_makefile and contains many variable
+# definitions, like the list of .v files or the path to Coq
+include makefile.conf
+
+# Put in place old names
+VFILES := $(COQMF_VFILES)
+MLIFILES := $(COQMF_MLIFILES)
+MLFILES := $(COQMF_MLFILES)
+MLGFILES := $(COQMF_MLGFILES)
+MLPACKFILES := $(COQMF_MLPACKFILES)
+MLLIBFILES := $(COQMF_MLLIBFILES)
+CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES)
+INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
+OTHERFLAGS := $(COQMF_OTHERFLAGS)
+COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS)
+OCAMLLIBS := $(COQMF_OCAMLLIBS)
+SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS)
+COQLIBS := $(COQMF_COQLIBS)
+COQLIBS_NOML := $(COQMF_COQLIBS_NOML)
+CMDLINE_COQLIBS := $(COQMF_CMDLINE_COQLIBS)
+LOCAL := $(COQMF_LOCAL)
+COQLIB := $(COQMF_COQLIB)
+DOCDIR := $(COQMF_DOCDIR)
+OCAMLFIND := $(COQMF_OCAMLFIND)
+CAMLFLAGS := $(COQMF_CAMLFLAGS)
+HASNATDYNLINK := $(COQMF_HASNATDYNLINK)
+OCAMLWARN := $(COQMF_WARN)
+
+makefile.conf:
+ coq_makefile -o makefile Util.v Bank.v Commands.v Requests.v Trace.v Arbiter.v FIFO.v
+
+# This file can be created by the user to hook into double colon rules or
+# add any other Makefile code he may need
+-include makefile.local
+
+# Parameters ##################################################################
+#
+# Parameters are make variable assignments.
+# They can be passed to (each call to) make on the command line.
+# They can also be put in makefile.local once and for all.
+# For retro-compatibility reasons they can be put in the _CoqProject, but this
+# practice is discouraged since _CoqProject better not contain make specific
+# code (be nice to user interfaces).
+
+# Print shell commands (set to non empty)
+VERBOSE ?=
+
+# Time the Coq process (set to non empty), and how (see default value)
+TIMED?=
+TIMECMD?=
+# Use command time on linux, gtime on Mac OS
+TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
+ifneq (,$(TIMED))
+ifeq (0,$(shell command time -f "" true >/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
+
+ifneq (,$(COQBIN))
+# add an ending /
+COQBIN:=$(COQBIN)/
+endif
+
+# Coq binaries
+COQC ?= "$(COQBIN)coqc"
+COQTOP ?= "$(COQBIN)coqtop"
+COQCHK ?= "$(COQBIN)coqchk"
+COQDEP ?= "$(COQBIN)coqdep"
+COQDOC ?= "$(COQBIN)coqdoc"
+COQPP ?= "$(COQBIN)coqpp"
+COQMKFILE ?= "$(COQBIN)coq_makefile"
+OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep"
+
+# 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=str,unix,dynlink,threads,zarith
+
+# 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 .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
+# 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)/user-contrib)
+COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable?
+
+########## 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?=
+
+# these flags do NOT contain the libraries, to make them easier to overwrite
+COQFLAGS?=-q $(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.13.1
+
+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))
+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
+
+# 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)
+# 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
+
+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)
+
+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 $(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.
+
+install:
+ $(HIDE)code=0; for f in $(FILESTOINSTALL); do\
+ if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \
+ done; exit $$code
+ $(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 "$(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 $(MLGFILES:.mlg=.ml)
+ $(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 -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) $(CAMLPKGS) $<
+
+$(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) $(CAMLPKGS) $<
+
+# Same hack
+$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
+ $(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
+ $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
+
+
+$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
+ $(SHOW)'CAMLOPT -shared -o $@'
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+ -linkall -shared -o $@ $<
+
+$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
+ $(SHOW)'CAMLC -a -o $@'
+ $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
+ $(SHOW)'CAMLOPT -a -o $@'
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+
+
+$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
+ $(SHOW)'CAMLOPT -shared -o $@'
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+ -shared -linkall -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
+ $(SHOW)'CAMLOPT -a -o $@'
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
+ $(SHOW)'CAMLC -a -o $@'
+ $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
+ $(SHOW)'CAMLC -pack -o $@'
+ $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
+ $(SHOW)'CAMLOPT -pack -o $@'
+ $(HIDE)$(TIMER) $(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) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
+ $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
+ $(HIDE)$(TIMER) $(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 -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 ,-f ,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES)
+
+$(VDFILE): $(VFILES)
+ $(SHOW)'COQDEP VFILES'
+ $(HIDE)$(COQDEP) -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 'LOCAL = $(LOCAL)'
+ @echo 'COQLIB = $(COQLIB)'
+ @echo 'DOCDIR = $(DOCDIR)'
+ @echo 'OCAMLFIND = $(OCAMLFIND)'
+ @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
+
+# Local Variables:
+# mode: makefile-gmake
+# End:
diff --git a/coq/makefile.conf b/coq/makefile.conf
new file mode 100644
index 0000000000000000000000000000000000000000..8c8f850274a86bc50b1b0a6b104b338731edfd13
--- /dev/null
+++ b/coq/makefile.conf
@@ -0,0 +1,55 @@
+# This configuration file was generated by running:
+# coq_makefile -o makefile Util.v Bank.v Requests.v Commands.v Trace.v Arbiter.v FIFO.v
+
+
+###############################################################################
+# #
+# Project files. #
+# #
+###############################################################################
+
+COQMF_VFILES = Util.v Bank.v Requests.v Commands.v Trace.v Arbiter.v FIFO.v
+COQMF_MLIFILES =
+COQMF_MLFILES =
+COQMF_MLGFILES =
+COQMF_MLPACKFILES =
+COQMF_MLLIBFILES =
+COQMF_CMDLINE_VFILES = Util.v Bank.v Requests.v Commands.v Trace.v Arbiter.v FIFO.v
+
+###############################################################################
+# #
+# Path directives (-I, -R, -Q). #
+# #
+###############################################################################
+
+COQMF_OCAMLLIBS = -I .
+COQMF_SRC_SUBDIRS = .
+COQMF_COQLIBS = -I . -R . sdram
+COQMF_COQLIBS_NOML = -R . sdram
+COQMF_CMDLINE_COQLIBS = -I . -R . sdram
+
+###############################################################################
+# #
+# Coq configuration. #
+# #
+###############################################################################
+
+COQMF_LOCAL=0
+COQMF_COQLIB=/home/brandner/.opam/default/lib/coq/
+COQMF_DOCDIR=/home/brandner/.opam/default/doc/
+COQMF_OCAMLFIND=/home/brandner/.opam/default/bin/ocamlfind
+COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67 -safe-string -strict-sequence
+COQMF_WARN=-warn-error +a-3
+COQMF_HASNATDYNLINK=true
+COQMF_COQ_SRC_SUBDIRS=config lib clib kernel library engine pretyping interp gramlib gramlib/.pack parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/ssrsearch plugins/syntax
+COQMF_COQ_NATIVE_COMPILER_DEFAULT=no
+COQMF_WINDRIVE=
+
+###############################################################################
+# #
+# Extra variables. #
+# #
+###############################################################################
+
+COQMF_OTHERFLAGS =
+COQMF_INSTALLCOQDOCROOT = Top