Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-04-17

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

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #isabelle
01:48 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/
08:53 pruvisto JCaesar: that might be feasible, I suppose
08:53 pruvisto it would require a huge unification net of all facts ever proven though
09:10 pruvisto the performance and memory overhead might not be worth it
09:11 pruvisto I think library facts are usually better referred to by name
09:11 pruvisto so that the proof still works if some minor detail changes
09:12 pruvisto also, library facts are usually too big to refer to them by content anyway
10:42 larsrh I mean, the reality is that the AFP has become larger than ever anticipated
10:42 larsrh so far we have been able to cope reasonably well
10:42 larsrh but there are so many unmaintainable proofs in there ...
10:43 larsrh The value proposition of Isar was (and is) that maintenance becomes easy because you know exactly where stuff breaks
10:43 larsrh and in AFP entries that are recent, that works as expected
11:16 ammbauer larsrh: you should do a blog post "apply style considered harmful" :D
12:01 pruvisto larsrh: we should create a "Bad AFP"
12:01 pruvisto and move all those entries to that
12:02 pruvisto and then we let it go bankrupt
12:02 larsrh pruvisto: I have argued for that in the past already :p
12:16 JCaesar Oh no, the Iptables_Semantics!
12:18 JCaesar Hm, would it be possible to take apply style proofs, turn each state into a have, organize them backwards, and that's it?
12:22 larsrh I have a student working on that
12:23 JCaesar competent?
12:27 larsrh I think so
12:49 pruvisto I'm not sure if that'll be a huge improvement
12:50 pruvisto at least certain people will suddenly have a /lot/ more LOC in the AFP then
14:18 dmiles joined #isabelle
14:20 dmiles joined #isabelle
14:32 dmiles joined #isabelle
18:13 ertesx joined #isabelle

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