Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-09-01

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
01:51 ilbot3 joined #isabelle
01:51 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
03:12 hazyPurple joined #isabelle
12:53 chindy how can i download/install the devel version of isabelel to verify that my theory also works for the new release?
12:56 pruvisto chindy: hg clone http://isabelle.in.tum.de/repos/isabelle/
12:56 pruvisto then ./bin/isabelle components -I, ./bin/isabelle components -a
12:56 pruvisto and then you can just start jedit with ./bin/isabelle jedit …
12:56 pruvisto although it will still have to build the Pure and HOL images, which will take a few minutes
12:57 pruvisto it's all described here: http://isabelle.in.tum.de/repos/isabelle/file/tip/README_REPOSITORY
13:06 chindy pruvisto:  ah thanks. Another question, when generating a proof document, how can I make isabelle not print the proofs and instead just writ <proof>
13:09 pruvisto hmm
13:09 pruvisto you can try something like -o document=theory
13:10 pruvisto no never mind
13:11 pruvisto -t /proof,/ML
13:11 pruvisto that should fold any proofs and ML stuff
13:13 chindy pruvisto: for which tools is that the argument?
13:13 chindy isabelle /isabelle builds does not recognise -t
13:23 pruvisto ah crap
13:23 pruvisto yeah that's an option for isabelle document
13:23 pruvisto which you are not supposed to call manually, normally
13:24 pruvisto -o document_variants=document:outline=/proof,/ML
13:24 pruvisto that works
13:24 pruvisto you just give it to isabelle build as an additional option
13:24 pruvisto that will generate both the "normal" document and an additional "outline" document with proofs and ML code folded
13:47 chindy pruvisto: so something like : isabelle build -o document_variants=document:outline=/proof,/ML -b -d .  ASDF
13:48 pruvisto yes
13:48 pruvisto you might need another -o document=pdf in there
13:48 pruvisto not sure
14:05 hazyPurple joined #isabelle
14:31 Warrigal_ joined #isabelle
14:47 hazyPurple joined #isabelle
18:32 hazyPurple joined #isabelle
22:14 Warrigal_ joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary