The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Benjamin,

"Benjamin C. Pierce" 
<bcpierce AT cis.upenn.edu>
 writes:

> Do you have automation there to automatically generate a jscoq
> instance for SF?

> I’d love to be able to point SF users to jscoq, as soon as it is ready
> (= as soon as someone can just follow one link and start doing
> exercises from the newest SF in their browser)...

SF is fully supported in jsCoq. It is a top priority for us to be sure
it works well and it is an important internal use case.

Building should be automated, the attached script should do the job
(requires OPAM).

I've put an online copy of the output at

https://x80.org/rhino-coq/examples/sf/

but IMHO it makes more sense for the copy to be hosted at UPenn.

I think it is not yet ready to the point you can fully replace
Emacs/CoqIDE, however it is a start and the thing can serve as backup.

Note that:

- You need change all the imports from

  "Require Import Tactics"

  to

  "Require Import SF.Tactics"

  etc...
  [I've fixed this by brute force in the online copy,
   but I'd recommend adding "-R . SF" to SF's Make]

- The UI is in a primitive state. It will be much improved in Coq 8.6.

  On the other hands, with the UI being written in Html/JS, the students
  may have a much better chance of contribute to it!

- The output of our modified CoqDoc (uDoc) leaves much to be desired.
  We are shifting efforts here towards more modern tools like Clément's
  Sphinx-based documentation tool, but it shouldn't be too hard to
  correct the few remaining hiccups.

Best regards,
Emilio

#!/bin/bash

set -x

# SF
wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tar.gz
tar xvfz sf.tar.gz
cd sf

# Udoc
opam install ocamlbuild

git clone -b sf https://github.com/ejgallego/udoc.git udoc
cd udoc && make && cd ..

UDOC=udoc/udoc.byte

# jscoq-builds
git clone --depth 1 https://github.com/ejgallego/jscoq-builds.git jscoq

# Build sf Htmls
for i in *.v
do
         $UDOC $i
done