Patch KeY: Export LaTeX logic proof

[Vincent]

ProofSaverLatex.java.gz

patch for KeY 1.4.0

(2.56 KiB) Downloaded 1788 times

This is a small, quick and dirty patch for the KeY prover (1.4.0), overriding the default (useless) LaTeX export mode.

KeY now exports nicely formatted logic proofs, using the nifty bussproofs bussproofs LaTeX package.

The proofs are annotated by rule names and, when relevant, variable instantiations.

Here is an automatically generated proof tree (edit: I noticed the branches appear in the wrong order; this has been corrected):

Instructions: replace existing ProofSaverLatex.java file in /key-1.4.0/system/de/uka/ilkd/key/proof. Recompile. To export in LaTeX mode, just save proof with .tex extension. Insert resulting TeX file in your document, which must use the package bussproofs.

[Benjamin DREUX]

to use this patch you will also need to use the latex package amsmath

[Vincent]

NOTE TP M1


on me signale que le patch bugge sur les preuves du second TP (avec les boucles).

Je n'ai prévu le patch que pour les formules de logique du premier ordre.

Je le mettrai à jour bientôt pour qu'il s'adapte aux preuves sur les boucles.


Ceci dit, les arbres de preuves ne sont pas demandés dans le second TP KeY. (ils sont beaucoup trop gros)

[Olivier FINOT]

Si certains ont encore des problèmes pour installer la version modifiée du Key Prover sous linux, voici un HowTo rédigé par frédéric spade

édit Vincent: citation du contenu du fichier (plus pratique que de le télécharger)

Pour installer KeY sous linux :

Ne pas mettre d'espaces dans les noms de répertoires !!!

Décompresser les trois archives : KeY-1.4.0-src.tgz, KeyExtLib-1.4.tgz et ProofSaverLatex.java.gz

Placer le contenu du répertoire : KeYExtLib-1.4 dans le répertoire key-1.4.0/key-ext-jars.

Placer le fichier ProofSaverLatex.java dans le répertoire : key-1.4.0/system/de/uka/ilkd/key/proof.

Depuis un terminal, se positionner dans le répertoire : key-1.4.0/system puis taper la commande : make

La compilation va s'exécuter pendant un certain temps, puis indiquera peut être plusieurs warning tout en indiquant que la compilation a réussi.

Ensuite, se placer dans le répertoire : key-1.4.0/bin puis lancer la commande : ./runProver

Le logiciel doit normalement se lancer.

Concernant la sauvegarder des arbres de preuve, il faut prouver une expression, ensuite la sauvegarder Ex : toto.key.proof et ajouter l'extansion : tex.

Ex : toto.key.proof.tex

Ne pas oublier d'inclure \usepackage{amsmath} et \usepackage{bussproofs} dans le fichier en cours de rédaction pour prendre en charge le code généré dans les fichiers x.key.proof.tex

[LatexNoob]

Je n'arrive pas à décaler mon arbre sur la gauche pour que tout s'affiche correctement.

J'ai essayé avec hspace*{-3cm}\begin{prooftree} ... \end{prooftree}
J'ai essayé également avec {minipage} mais sans succès également.

[Vincent]

Exemple de décalage (deux centimètres vers la gauche):

Code: Select all

\hspace*{-2cm}\begin{minipage}{21cm}
.... le contenu ....
\end{minipage}

[ninfomane]

J'ai mis ça :
\hspace*{-2cm}\begin{minipage}{21cm}
\input{4/proof-man.key.proof}
\end{minipage}

Mais ça me décale les arbres sur le texte. Ca fait pas beau quoi.
Y a une astuce ?! ^o)

[Vincent]

ça me décale les arbres sur le texte.

Je ne vois pas trop ce que tu veux dire Etant donné que tu ne me cites que le code que j'ai donné, qui est correct, le problème vient de ce qu'il y a autour...

Donc je vais sortir ma boule de cristal et essayer de deviner ce que tu as pu mettre autour.


Ma boule de cristakl me dit que tu as fait ceci

Code: Select all

ton texte \hspace........

ou

Code: Select all

ton texte
\hspace....

attention: un retour à la ligne simple est ignoré par LaTeX. L'environnement minipage met tout son contenu dans un seul "bloc", donc avec ce code, l'arbre devient partie intégrante de la ligne courante... et peut recouvrir le texte.

L'"astuce" consiste à mettre une ligne blanche entre le texte et l'environnement; ce qui revient à dire à LaTeX que l'arbre est sur un nouveau paragraphe.

Code: Select all

ton super texte...

\hspace*{-2cm}\begin{minipage}{21cm}
\input{4/proof-man.key.proof}
\end{minipage}