Last active
July 29, 2016 10:19
-
-
Save yforster/e7d73135aea3ef5e39e1e7272e53e568 to your computer and use it in GitHub Desktop.
How to use coqdocjs with proviola
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/bin/sh | |
coqtop -R . "" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
*** coqdoc_reader.py 2011-06-23 20:06:18.000000000 +0200 | |
--- coqdoc_reader-2.py 2016-07-29 12:17:05.584898246 +0200 | |
*************** | |
*** 78,86 **** | |
commands = self._find_commands(child) | |
if commands and self.isCommand(commands[0]): | |
command = self._replace_html(commands[0]) | |
! response = self._prover.send( | |
! command.encode(self._coqdoc_tree.originalEncoding)) | |
! | |
frame = Coqdoc_Frame(command = command, command_cd = coqdoc, | |
response = response) | |
frames.append(frame) | |
--- 78,85 ---- | |
commands = self._find_commands(child) | |
if commands and self.isCommand(commands[0]): | |
command = self._replace_html(commands[0]) | |
! if (command.count("Notation") == 0): | |
! response = self._prover.send(command.encode(self._coqdoc_tree.originalEncoding)) | |
frame = Coqdoc_Frame(command = command, command_cd = coqdoc, | |
response = response) | |
frames.append(frame) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/bin/sh | |
# Download proviola (http://mws.cs.ru.nl/proviola/files/proviola.tar.gz) | |
# apply the provided patch file to coqtop_reader.py | |
# then make the following line point to the unzipped directory | |
PROVIOLA="/home/user/Code/proviola" | |
# By default the outputfiles will be placed in a new directory called html-proviola | |
OUTPUTDIR="html-proviola/" | |
# Add -R and -I directives in the coqtop-adapted file | |
# Run coqdocjs (https://github.com/tebbi/coqdocjs) and copy all .html files in the html folder to the same folder where youre .v files are files are | |
# Leave the rest as it is and run this script as "proviola-coqdocjs file.html" | |
CAMERA="$PROVIOLA/camera/camera.py --coqtop ./coqtop-adapted" | |
CSS="$PROVIOLA/proviola/ppcoqdoc" | |
FILENAME=$(basename $1) | |
FILENAME="${FILENAME%.*}" | |
mkdir -p $OUTPUTDIR | |
$CAMERA $1 | |
cp $CSS/proviola.xsl . | |
cp $CSS/proviola.css $OUTPUTDIR | |
xsltproc $FILENAME.flm > $OUTPUTDIR/$FILENAME.html | |
rm $FILENAME.flm | |
cp config.js coqdoc.css coqdocjs.css coqdocjs.js $OUTPUTDIR | |
sed -i '/<link href="proviola.css" type="text\/css" rel="stylesheet">/c\<link href="proviola.css" type="text\/css" rel="stylesheet">\n<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>\n<script type="text/javascript" src="config.js"></script>\n<script type="text/javascript" src="coqdocjs.js"></script>' $OUTPUTDIR$FILENAME.html |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment