Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-04-16

| 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/
18:13 ertesx joined #isabelle
19:52 JCaesar wow. sledgehammer just came up with a three-step isar-proof. it's exactly the proof I would have written.
19:54 pruvisto nice
19:54 int-e welcome to the future where proofs write themselves
19:56 pruvisto I for one use sledgehammer more as a "fact searching machine"
19:57 int-e I'm hearing that a lot.
19:59 pruvisto the proofs it comes up with are typically "apply (metis …)" where "…" is a shit tonne of facts no one ever uses
20:00 pruvisto like my personal favourite "semiring_normalization_rules(34)"
20:00 pruvisto I find those ugly and hard to debug
20:00 pruvisto although lately, it often comes up with reasonable invocations of "simp" and "blast"
20:09 int-e should I feel bad about sometimes writing metis proofs by hand... (mostly this happens for straightforward equational reasoning... where the same equation needs to be applied in different directions, so simp doesn't work)
20:10 pruvisto I don't know. It's okay, I guess.
20:10 fds_ joined #isabelle
20:10 pruvisto But you should keep in mind that whenever one of the named facts in that invocation gets renamed or changes in some subtle way, that proof might break
20:11 pruvisto and the person who has to fix it may curse you for it
20:11 fds joined #isabelle
20:11 pruvisto and that person may be you
20:18 int-e I'd probably shy away from picking the 34th of a named set of simplification rules :)
20:40 ammbauer joined #isabelle
21:29 pruvisto 43 occurrences of "semiring_normalization_rules" in the AFP alone :D
21:36 JCaesar well, don't touch it.
21:50 larsrh increasingly this becomes a problem in the distribution
21:56 pruvisto larsrh: what exactly
22:04 larsrh pruvisto: fear of changing things due to fallout in the AFP
22:19 int-e . o O ( Isabelle/HOL-stable )
22:27 JCaesar I mean, one thing that would be nice for this: if you could refer to facts with `foo` instead of the lemma name…

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