Patch KeY: Export LaTeX logic proof

Some of the small programs I wrote on my spare time. They are Free Software, and written mostly in OCaml.
User avatar
Vincent
Posts: 3041
Joined: Fri Apr 07, 2006 12:10 pm
Location: Schtroumpf
Contact:

Patch KeY: Export LaTeX logic proof

Postby Vincent » Fri Apr 10, 2009 8:44 pm

ProofSaverLatex.java.gz
patch for KeY 1.4.0
(2.56 KiB) Downloaded 1119 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):Image

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.
Attachments
proof.png
automatically generated proof tree
Last edited by Vincent on Wed Jan 09, 2013 6:26 pm, edited 2 times in total.
Reason: link
{ Vincent Hugot }

Benjamin DREUX
Automate d'Interface
Posts: 104
Joined: Sun Sep 21, 2008 1:04 pm

Re: Patch KeY: Export LaTeX logic proof

Postby Benjamin DREUX » Wed Apr 15, 2009 3:31 pm

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

User avatar
Vincent
Posts: 3041
Joined: Fri Apr 07, 2006 12:10 pm
Location: Schtroumpf
Contact:

Re: Patch KeY: Export LaTeX logic proof

Postby Vincent » Thu Apr 16, 2009 11:07 am

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)
{ Vincent Hugot }

User avatar
Olivier FINOT
Membre projet CRT
Posts: 136
Joined: Mon Sep 22, 2008 7:22 pm

Re: Patch KeY: Export LaTeX logic proof

Postby Olivier FINOT » Thu Apr 16, 2009 11:40 am

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)
Fred wrote: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
Attachments
HowTo.txt
(1.1 KiB) Downloaded 1065 times
Last edited by Vincent on Thu Apr 16, 2009 1:48 pm, edited 1 time in total.
Reason: citation du contenu
En effet le rire n'est jamais gratuit, l'homme donne à pleurer, mais il prête à rire. (Desproges)

LatexNoob

Re: Patch KeY: Export LaTeX logic proof

Postby LatexNoob » Thu Apr 16, 2009 2:49 pm

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.

User avatar
Vincent
Posts: 3041
Joined: Fri Apr 07, 2006 12:10 pm
Location: Schtroumpf
Contact:

Re: Patch KeY: Export LaTeX logic proof

Postby Vincent » Thu Apr 16, 2009 4:16 pm

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

Code: Select all

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

ninfomane

Re: Patch KeY: Export LaTeX logic proof

Postby ninfomane » Fri Apr 17, 2009 3:51 pm

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)

User avatar
Vincent
Posts: 3041
Joined: Fri Apr 07, 2006 12:10 pm
Location: Schtroumpf
Contact:

Re: Patch KeY: Export LaTeX logic proof

Postby Vincent » Fri Apr 17, 2009 4:52 pm

ninfomane wrote:ç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}
{ Vincent Hugot }


Return to “Programs”

Who is online

Users browsing this forum: Bing [Bot] and 15 guests