The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

In the meantime, you can find our partially finished new draft here:

  http://www.cis.upenn.edu/~bcpierce/sf/sf-4.0/index.html

Up through Poly is quite stable now.  Tactics will be finished today, maybe also Logic.

Please let me know if you see anything to be fixed.

    - B

On Jan 29, 2016, at 2:44 PM, Mitchell Wand <wand AT ccs.neu.edu> wrote:

I'm trying to relearn Coq by going through SF version 3.2 (January 2015).

1. make failed at Poly.v .  I added "Set Asymmetric Patterns", which fixed this.

2. make failed again at MoreLogic.v, with the message

coqc  -q  -I .    MoreLogic

File ".\MoreLogic.v", line 3, characters 15-21:

Syntax error: [constr:global] expected after [export_token] (in [vernac:gallina_ext]).

Makefile:202: recipe for target 'MoreLogic.vo' failed

make: *** [MoreLogic.vo] Error 1

The file starts with Require Export "Prop".

I tried removing the quotation marks, and got the following:

$ make

coqdep -c -slash -I .  "MoreLogic.v" > "MoreLogic.v.d" || ( RV=$?; rm -f "MoreLogic.v.d"; exit ${RV} )

warning: option -slash has no effect and is deprecated.

*** Warning: in file MoreLogic.v, library Prop is required and has not been found in the loadpath!

*** Warning: in file MoreLogic.v, library Prop is required and has not been found in the loadpath!

coqc  -q  -I .    MoreLogic

File ".\MoreLogic.v", line 3, characters 15-19:

Syntax error: [constr:global] expected after [export_token] (in [vernac:gallina_ext]).

Makefile:202: recipe for target 'MoreLogic.vo' failed

make: *** [MoreLogic.vo] Error 1

This despite

$ ls Prop*

Prop.glob  Prop.html  Prop.v  Prop.v.d  Prop.vo

How can I fix this?

More generally, is there an up-to-date version of SF that runs out of the box in 8.5 ?

--Mitch