Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-08-20

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

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01: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/
06:21 larsrh chuchuco1ny: no, you can't update stable
06:22 larsrh that's why it's called stable
06:22 larsrh you can update devel, this is why it's called devel
10:47 chuchuco1ny :(
10:57 silver joined #isabelle
14:18 silver_ joined #isabelle
14:27 JCaesar Is there a simple example somewhere where a fact is checked (by eval, or something) and then exported, from ML code?
18:55 ThreeOfEight JCaesar: have a look at the regexp method in the AFP
18:56 ThreeOfEight https://www.isa-afp.org/browser_info/current/AFP/Regular-Sets/Regexp_Method.html
18:56 ThreeOfEight that also uses reification
18:57 ThreeOfEight Code_Runtime.static_holds_conv is basically eval
18:57 ThreeOfEight (albeit a version of eval where you have to give a list of all constants that may occur in the goal)
18:57 ThreeOfEight there's also Code_Runtime.dynamic_holds_conv where you don't have to do that, but that always uses the current code setup, not the code setup at the time the method was defined
18:58 ThreeOfEight so that is not recommended for production
18:58 ThreeOfEight cf. also https://isabelle.in.tum.de/dist/Isabelle2016/doc/codegen.pdf, especially section 5.3
22:04 ThreeOfEight joined #isabelle

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