examples/cont makefile

[andrew-appel]

On 12/15/2014 8:11 PM, [email protected] wrote:

Just wanted to let you know that the [cont] directory makefile doesn’t seem to work as is on my system. I needed to add [-I path/to/compcert -as compcert] to the command line flags for [coqc].

[llbit]

I am having problems building this example with the latest version of VST (commit 1745a39):

coqc -I . -I ../../msl -as msl -R ../../compcert -as compcert ../../msl/rmaps.v
coqc: -as: no such file or directory
make: *** [../../msl/rmaps.vo] Error 

I am using Coq 8.6.

I looked at the coqc documentation and it looks like they removed the -as flag, and this seems to work better:

COQFLAGS= -I . -Q ../../msl msl -R ../../compcert compcert

However compilation fails when building:

rm -f *.vo *~
rm -f language.html seplogic.html lift_seplogic.html model.html lseg.html client_lemmas.html sample_prog.html
rm -f language.glob seplogic.glob lift_seplogic.glob model.glob lseg.glob client_lemmas.glob sample_prog.glob
coqc -I . -Q ../../msl msl -R ../../compcert compcert language.v
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
File "./language.v", line 59, characters 0-36:
Warning: Implicit Arguments is deprecated; use Arguments instead
[deprecated-implicit-arguments,deprecated]
coqc -I . -Q ../../msl msl -R ../../compcert compcert seplogic.v
coqc -I . -Q ../../msl msl -R ../../compcert compcert lift_seplogic.v
coqc -I . -Q ../../msl msl -R ../../compcert compcert ../../msl/rmaps.v
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
File "../../msl/rmaps.v", line 57, characters 23-36:
Error: Illegal application (Non-functional construction): 
The expression "functor" of type "Type"
cannot be applied to the term
 "preds" : "Type -> Type"
make: *** [../../msl/rmaps.vo] Error 1