Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-05-04

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

All times shown according to UTC.

Time Nick Message
00:20 mbrcknl joined #isabelle
01:49 ilbot3 joined #isabelle
01:49 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:24 ertes joined #isabelle
07:43 ertes-w joined #isabelle
07:51 dave24 joined #isabelle
12:24 chindy pruvisto: i meant people working on "meta verification" of Isabelle ... also the inner working of Isabelle i.e. concerns as to why its not entirely LCF ...
12:26 chindy Basically I read Tom Hales "Formal Proof" where he briefly disects HOL Light and lists a few papers with more detailed results, and i was wondering if something like that exists for Isabelle, or where I can read up on something similar
13:07 ertes joined #isabelle
14:31 ertes joined #isabelle
14:43 int-e Hmpf. I have a proof where  apply standard; apply simp  works but  apply auto  loops, just importing Main from HOL, no additional rules... (I'll hit the mailing list with this if it still happens in "the" development version).
14:44 int-e I never know how to debug these things
14:45 int-e (the simp trace doesn't look helpful; I suspect it's not the simplifier that's looping)
14:46 pruvisto hard to say without knowing what the goal looks like
14:51 int-e still happens in the development version, yay(?)
14:52 int-e (mail sent)
14:54 int-e (or perhaps not... my mail setup broke)
14:56 int-e oh well, that may take a while. in the meantime, if anybody wants to play with it, here's the theory: http://downthetypehole.de/paste/JvfKUlLJ
15:09 ertes-w joined #isabelle
22:12 ertes joined #isabelle
23:42 dmiles joined #isabelle

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