Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-11-14

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

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #isabelle
02:47 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/
02:59 tokenrove joined #isabelle
05:10 int-e_ joined #isabelle
05:13 tokenrov1 joined #isabelle
05:53 ilbot3 joined #isabelle
05:53 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/
06:24 ilbot3 joined #isabelle
06:24 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/
07:05 ThreeOfEight joined #isabelle
07:05 rofer joined #isabelle
07:45 kyagrd_ joined #isabelle
08:23 kyagrd_ joined #isabelle
09:02 keep_learning joined #isabelle
09:03 keep_learning Hello everyone
09:04 keep_learning I am trying to start with Isabelle and following http://www.inf.ed.ac.uk/teaching/courses/ar/isabelle/isabelle-startup.pdf
09:04 keep_learning I wrote the code
09:04 keep_learning but getting
09:04 keep_learning Inner lexical error⌂ Failed to parse prop
09:05 keep_learning http://lpaste.net/145224
09:19 kyagrd_ hmm I think it is best to just install Isabelle2015
09:20 kyagrd_ I am a new to isablell myself (used HOL vairants a little before)
09:21 kyagrd_ and the linux package just wored for me
09:22 kyagrd_ Once you successfuly installed the 2015 distribution, go to the documentation section of the jedit IDE envoronment and follow the "programming and proving in Isabelle" tutorial
09:25 kyagrd_ About your lpaste it should be "A ==> A \/ B"
09:26 kyagrd_ --> is also possible but ==> is recommended
09:26 kyagrd_ the reason for that will be explained if you follow that tutorial I mentioend
09:27 kyagrd_ That's the only experience in Isabelle so far BTW :)
09:27 keep_learning kyagrd_: Thank you
09:27 kyagrd_ -> is a connnective for function type. --> is an implication ==> is something else ... but preferred for top level lemma/theorem statements.
09:29 kyagrd_ Jedit IDE is so cool. Just way more friendly and it is based on a real text editor unlike CoqIDE.
09:29 kyagrd_ BTW, I also have a question for more experienced Isabelle users.
09:30 keep_learning kyagrd_: I tried to first work with emacs and PG but it did not work well
09:30 keep_learning so using jedit
09:30 kyagrd_ I am not a good emacs user so I avoid PG as much as possible
09:31 kyagrd_ In more primitive HOL like hol-light, one usually make a snapshot of the memory status because HOL does not have proof terms, so in order to save the proof state HOL sysetms usually make a memory snapshot image using utilities for that.
09:31 ThreeOfEight PG for Isabelle, unfortunately, is pretty much dead.
09:32 kyagrd_ Isabelle seems to have extended HOL to have proof terms (am I correct about this). And just curious what is the standard way to save the state so I don't have to re-compute the proof every time I open the thy file again?
09:32 ThreeOfEight you /can/ have proof terms in Isabelle, but they are rarely used because (from what I've heard) they are huge and make things slow.
09:32 ThreeOfEight Isabelle also uses memory snapshots for most things.
09:33 ThreeOfEight like, by default, there is a "HOL" heap image (i.e. a dump of the ML memory) that is loaded on startup so you don't have to process it all again
09:33 ThreeOfEight that's basically the "standard library" of Isabelle/HOL
09:33 ThreeOfEight you can also make your own session heaps
09:33 kyagrd_ ThreeOfEight: does jedit IDE has a menu for that? about configuring "session heap"
09:58 ThreeOfEight kyagrd_: creating images? no I don't think so.
09:58 ThreeOfEight I think you do that with isabelle build
10:00 kyagrd_ So, I would be loading two images then, the HOL image and my own session image? Or, is it always one heap image?
10:01 kyagrd_ ah, it seems that I have to make up a ROOT.ML file
10:06 ThreeOfEight no, it's always one
10:07 ThreeOfEight (there is some work in progress on hierarchical heap images, but we're not there yet)
10:08 ThreeOfEight the problem, of course, is that every time you make a tiny change in one of the theories in the image, you have to rebuild the entire image
10:08 kyagrd_ I think there should be a tutiorial on this session/heap image for beginning users. It is quite tricky to figure these kind of things
10:09 ThreeOfEight well you don't really need to worry about these things as a beginner
10:09 ThreeOfEight heap images are only really relevant when you have theories with several thousand lines
12:54 kyagrd ThreeOfEight: when I get lazy I just run try and sledgehammer finds somthing calling smt solver, and those proofs tend to take some time. When I re-open those file with those kind of lazily sledgehammered proofs, running those exteral solver hooked proofs takes quite some time.
12:54 kyagrd In that case I wich I had made a snapshot
12:55 kyagrd s/wich/wish/
12:58 ThreeOfEight yeah, I wouldn't recommend that

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