1:BUILD_BY[name] student4
1:BUILD_ENVIRONMENT[operating system 32 vs 64]

1:END_BUILD_ENVIRONMENT
1:DEPENDENCIES[list of dependencies with where to get them]
Coq (proof assistant)
+ got aptitude from apt-get
+ next$ sudo aptitude install coq
Ocaml compiler
+ sudo apt-get install ocaml
Also needed ocamlc
and camlp5
and ocaml-native-compilers
1:END_DEPENDENCIES
1:NOTES[notes on attempted build]
After installing all dependencies ran make in directory
output:
student@ubuntu:~/test_repro/relax$ make                                                                    
coqc  -q  -I .    AssertionLogic                                                                        
NoDup_nil: forall A : Type, NoDup nil                                                                   
NoDup_cons:                                                                                             
  forall (A : Type) (x : A) (l : list A),                                                               
  ~ In x l -> NoDup l -> NoDup (x :: l)                                                                 
NoDup_ind:                                                                                              
  forall (A : Type) (P : list A -> Prop),                                                               
  P nil ->                                                                                              
  (forall (x : A) (l : list A), ~ In x l -> NoDup l -> P l -> P (x :: l)) ->                            
  forall l : list A, NoDup l -> P l                                                                     
NoDup_remove_1:                                                                                         
  forall (A : Type) (l l' : list A) (a : A),                                                            
  NoDup (l ++ a :: l') -> NoDup (l ++ l')                                                               
NoDup_remove_2:
  forall (A : Type) (l l' : list A) (a : A),
  NoDup (l ++ a :: l') -> ~ In a (l ++ l')
nodup_map:
  forall (A B : Type) (f : A -> B),
  (forall x y : A, f x = f y -> x = y) ->
  forall l : list A, NoDup l -> NoDup (map f l)
gen_numbers_nodup: forall n start : nat, NoDup (gen_numbers n start)
coqc  -q  -I .    Substitution
coqc  -q  -I .    UnaryAssertionLogic
pred_swap_subst:
  forall (s : selector) (P : pred) (x : bvar) (n : nat),
  pred_subst_var (pred_swap P) x s n =
  pred_swap (pred_subst_var P x (select selector s Right Left) n)
pred_swap_denote:
  (forall (P : pred) (env1 env2 : environment),
   pred_denote P env1 env2 -> pred_denote (pred_swap P) env2 env1) /\
  (forall (P : pred) (env1 env2 : environment),
   npred_denote P env1 env2 -> npred_denote (pred_swap P) env2 env1)
pred_swap_free_vars:
  forall P : pred, pred_free_vars (pred_swap P) Right = pred_free_vars P Left
pred_array_free_pred_swap:
  forall P : pred,
  pred_array_free P Left -> pred_array_free (pred_swap P) Right
coqc  -q  -I .    Orig inalAxiomatic
Axioms:
functional_extensionality_dep : forall (A : Type) (B : A -> Type)
                                  (f g : forall x : A, B x),
                                (forall x : A, f x = g x) -> f = g
Axioms:
functional_extensionality_dep : forall (A : Type) (B : A -> Type)
                                  (f g : forall x : A, B x),
                                (forall x : A, f x = g x) -> f = g
coqc  -q  -I .    RelaxedDynamic
coqc  -q  -I .    IntermediateAxiomatic
Axioms:
functional_extensionality_dep : forall (A : Type) (B : A -> Type)
                                  (f g : forall x : A, B x),
                                (forall x : A, f x = g x) -> f = g
make: *** No rule to make target `RelaxedAxiomatic.vo', needed by `all'.  Stop.

not sure where to go from here.
1:END_NOTES



2:BUILD_BY[name] student8
2:BUILD_ENVIRONMENT[operating system 32 vs 64] Ubuntu 12.04 64-bit

2:END_BUILD_ENVIRONMENT
2:DEPENDENCIES[list of dependencies with where to get them]

sudo apt-get install coq
sudo apt-get install camlp5
sudo apt-get install ocaml-native-compilers

2:END_DEPENDENCIES
2:NOTES[notes on attempted build]

$ make
...
make: *** No rule to make target `RelaxedAxiomatic.vo', needed by `all'.  Stop.

RelaxedAxiomatic.v and WeakestPreconditions.v are missing (in Makefile but not in
source directory).

Tried to remove them from the Makefile and "make" ran without any problems and got the results.

$ make
$ make
coqdep -c -slash -I .  "IntermediateAxiomatic.v" > "IntermediateAxiomatic.v.d" || ( RV=$?; rm -f "IntermediateAxiomatic.v.d"; exit ${RV} )
coqdep -c -slash -I .  "Substitution.v" > "Substitution.v.d" || ( RV=$?; rm -f "Substitution.v.d"; exit ${RV} )
coqdep -c -slash -I .  "UnaryAssertionLogic.v" > "UnaryAssertionLogic.v.d" || ( RV=$?; rm -f "UnaryAssertionLogic.v.d"; exit ${RV} )
coqdep -c -slash -I .  "AssertionLogic.v" > "AssertionLogic.v.d" || ( RV=$?; rm -f "AssertionLogic.v.d"; exit ${RV} )
coqdep -c -slash -I .  "RelaxedDynamic.v" > "RelaxedDynamic.v.d" || ( RV=$?; rm -f "RelaxedDynamic.v.d"; exit ${RV} )
coqdep -c -slash -I .  "Origi nalAxiomatic.v" > "Origi nalAxiomatic.v.d" || ( RV=$?; rm -f "Origi nalAxiomatic.v.d"; exit ${RV} )
coqdep -c -slash -I .  "Origi nalDynamic.v" > "Origi nalDynamic.v.d" || ( RV=$?; rm -f "Origi nalDynamic.v.d"; exit ${RV} )
coqdep -c -slash -I .  "Language.v" > "Language.v.d" || ( RV=$?; rm -f "Language.v.d"; exit ${RV} )
coqdep -c -slash -I .  "Statements.v" > "Statements.v.d" || ( RV=$?; rm -f "Statements.v.d"; exit ${RV} )
coqdep -c -slash -I .  "Expressions.v" > "Expressions.v.d" || ( RV=$?; rm -f "Expressions.v.d"; exit ${RV} )
coqdep -c -slash -I .  "Tactics.v" > "Tactics.v.d" || ( RV=$?; rm -f "Tactics.v.d"; exit ${RV} )
coqdep -c -slash -I .  "util.v" > "util.v.d" || ( RV=$?; rm -f "util.v.d"; exit ${RV} )
coqdep -c -slash -I .  "CpdtTactics.v" > "CpdtTactics.v.d" || ( RV=$?; rm -f "CpdtTactics.v.d"; exit ${RV} )
coqc  -q  -I .    CpdtTactics
coqc  -q  -I .    util
coqc  -q  -I .    Tactics
coqc  -q  -I .    Expressions
coqc  -q  -I .    Statements
coqc  -q  -I .    Language
coqc  -q  -I .    Origi nalDynamic
coqc  -q  -I .    AssertionLogic
NoDup_nil: forall A : Type, NoDup nil
NoDup_cons:
  forall (A : Type) (x : A) (l : list A),
  ~ In x l -> NoDup l -> NoDup (x :: l)
NoDup_ind:
  forall (A : Type) (P : list A -> Prop),
  P nil ->
  (forall (x : A) (l : list A), ~ In x l -> NoDup l -> P l -> P (x :: l)) ->
  forall l : list A, NoDup l -> P l
NoDup_remove_1:
  forall (A : Type) (l l' : list A) (a : A),
  NoDup (l ++ a :: l') -> NoDup (l ++ l')
NoDup_remove_2:
  forall (A : Type) (l l' : list A) (a : A),
  NoDup (l ++ a :: l') -> ~ In a (l ++ l')
nodup_map:
  forall (A B : Type) (f : A -> B),
  (forall x y : A, f x = f y -> x = y) ->
  forall l : list A, NoDup l -> NoDup (map f l)
gen_numbers_nodup: forall n start : nat, NoDup (gen_numbers n start)
coqc  -q  -I .    Substitution
coqc  -q  -I .    UnaryAssertionLogic
pred_swap_subst:
  forall (s : selector) (P : pred) (x : bvar) (n : nat),
  pred_subst_var (pred_swap P) x s n =
  pred_swap (pred_subst_var P x (select selector s Right Left) n)
pred_swap_denote:
  (forall (P : pred) (env1 env2 : environment),
   pred_denote P env1 env2 -> pred_denote (pred_swap P) env2 env1) /\
  (forall (P : pred) (env1 env2 : environment),
   npred_denote P env1 env2 -> npred_denote (pred_swap P) env2 env1)
pred_swap_free_vars:
  forall P : pred, pred_free_vars (pred_swap P) Right = pred_free_vars P Left
pred_array_free_pred_swap:
  forall P : pred,
  pred_array_free P Left -> pred_array_free (pred_swap P) Right
coqc  -q  -I .    Origi nalAxiomatic
Axioms:
functional_extensionality_dep : forall (A : Type) (B : A -> Type)
                                  (f g : forall x : A, B x),
                                (forall x : A, f x = g x) -> f = g
Axioms:
functional_extensionality_dep : forall (A : Type) (B : A -> Type)
                                  (f g : forall x : A, B x),
                                (forall x : A, f x = g x) -> f = g
coqc  -q  -I .    RelaxedDynamic
coqc  -q  -I .    IntermediateAxiomatic
Axioms:
functional_extensionality_dep : forall (A : Type) (B : A -> Type)
                                  (f g : forall x : A, B x),
                                (forall x : A, f x = g x) -> f = g

I can also use "make COQ_XML=-xml" to export the theories to XML.

2:END_NOTES