search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Precompiled PDF of ref manual would be very helpful #231

Open jcamins opened 10 years ago

jcamins commented 10 years ago

The reference manual is provided only as a K file (that contains only LaTeX, but needs to be preprocessed by K somehow before it can be used), but there are no instructions for compiling the reference manual. The barrier for entry would be greatly lowered if there were a PDF of the manual available for printing, etc.

denis-bogdanas commented 10 years ago

An attempt to compile the manual produces an exception:

d:\k-framework\documentation>kompile --backend pdf ref-manual.k Exception in thread "main" java.lang.NullPointerException

version: bcbfff7 Platform: windows

denis-bogdanas commented 10 years ago

d:\k-framework\documentation>kompile.bat --backend pdf ref-manual.k [Warning] Compiler: pdflatex returned a non-zero exit code. The pdf might be generated, but with bugs. please inspect the latex logs.

d:\k-framework\documentation>kompile --version K-framework nightly build. Git Revision: 2d8f90d Build date: Thu May 15 16:46:23 CDT 2014

dwightguth commented 9 years ago

Oncall needs to fix the compilation errors.

dwightguth commented 9 years ago

There are now instructions to build the pdf: however, it still needs to be made to build automatically. Additionally, the pdf needs at some point to be updated with the latest version of K and synced with the to-be-processed.

WalkerCodeRanger commented 9 years ago

Tried to follow instructions to build ref manual for v3.5.2 on windows. It failed. Really need the prebuilt pdf. Seems like k project is exactly what I need, but the documentation is so inaccessible and lacking I am having a lot of trouble getting started. If I can't get past these issues I may have to use a different tool.

DustinWehr commented 6 years ago

So does nobody have a build of the ref manual that they can upload somewhere??? Ditto for pdfs built from all the latex in the tutorial examples. I am trying to evaluate whether my company should use K, and having to successfully install everything (I too have failed to build the reference manual) before I can even read the formatted documentation is a BIG red flag.

grosu commented 6 years ago

@DustinWehr Unfortunately, as an academic team we didn't have the resources to maintain the reference manual. A demotivating factor for that was also the fact that K changed a lot lately. In fact, we are working on a new backend of K implemented in Haskell, targeted for proofs and the generation of proof objects to serve as correctness certificates for smart contracts or any other programs.

If your plan is to use K only to implement executable semantics of languages, then the current version will serve your purposes well. There are tons of example semantics in K and a tutorial, which should be enough to learn how to use it. And we will also be very responsive.

But if your plan is to do proofs with K, then we will need to work more closely together on it, because this is a moving target and not well documented. You are also more than welcome to help with the new Haskell backend, which will be great at proofs. We expect to have it working in a few months. We also have support and help from IOHK to do this.

DustinWehr commented 6 years ago

@grosu Thank you for that fast response! Is the compilation to pdf of the latex in the literate programming tutorial examples not working, then? I've tried with the kompile command from one of the videos, and a little with kdoc based on the --help.

Very cool that you're working with IOHK! I bought a little ADA a week ago, luckily (for now). This sounds interesting. The company I work for: https://legalese.com/ We have a prototype of our language/system L4 for computational legal contracts, but we're not attached to it. Main features will be natural language generation, testing, formal verification, visualization. And generation of smart contracts, if our funders remain interested in that. @mengwong @virgil

DustinWehr commented 6 years ago

@grosu I forgot to say in my last message; proofs would indeed be our primary reason for using K. I'm looking at https://runtimeverification.com/blog/?p=496 and wondering how far along the Deductive Program Verifier, Symbolic Execution, and Model Checker components are.

Is Github issues the right place for questions about the formal verification aspects of K?