Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2014-11-06

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

All times shown according to UTC.

Time Nick Message
13:58 cheater__ joined #isabelle
14:36 cheater hi
14:37 cheater when using isabelle/hol, do you only ever use the (jedit?) ide, or is it possible to compile the code as well and look whether the proof works there?
14:52 Jafet Other ways to run theory scripts are "build" and "tty".
14:53 Jafet There is nothing wrong with using isabelle/jedit to see whether the proof "works", though.
15:35 cheater__ joined #isabelle
15:36 cheater Jafet: right. I'm just thinking of the case where e.g. a build system depends on the proofs being correct.
16:12 Jafet Use isabelle build.

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