Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-08-22

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

All times shown according to UTC.

Time Nick Message
03:09 dmiles joined #isabelle
06:58 ThreeOfEight ammbauer: if you do need concrete help with understanding HOL Light proofs and have no better help available, do feel free to ask me
06:58 ThreeOfEight I've never actually used HOL Light, but I have ported some proofs from it to Isabelle
07:56 silver joined #isabelle
09:45 int-e Well, this was a fun error message to tryn and understand: http://sprunge.us/aZKi (I'll probably send a bug report later, carefully avoiding the word "bug")
09:54 ThreeOfEight I see you learnt the first rule of the Isabelle mailing list :P
09:55 ThreeOfEight What caused that error message?
09:56 int-e ThreeOfEight: there is a theory called "Fun" in the HOL image, and loading the Multiset theory transitively loads Main, and then, I believe, a theory merge step goes wrong.
09:56 int-e If one imports Main directly one gets a far better error message.
10:01 ThreeOfEight oh I see
10:01 ThreeOfEight I wasn't sure whether your theory being named "Fun" was part of the problem you wanted to illustrate
10:02 ThreeOfEight when I saw that it was named "Fun", that was my first thought
10:02 ThreeOfEight I agree that this is awful error reporting behaviour
10:02 ThreeOfEight In general, the error reporting w.r.t. file loading could be a lot better
10:03 ThreeOfEight (In fact, the entire concept of theory namespaces could be a lot better, but I fear it will be at least a decade before we get there)
10:03 ThreeOfEight (perhaps never)
10:04 ThreeOfEight (although, on second thought, seeing as the low-level naming details are hidden through @{const_name} antiquotations in good coding style, it may be feasible)
12:13 JCaesar ammbauer: https://ci.isabelle.systems/afp-submission/ the submit-button here, that builds it first and doesn't send any mails immediately, right?
12:20 larsrh JCaesar: a mail is only send to the AFP editors when you click on the link in the "build successful" mail
12:20 larsrh *sent
12:21 larsrh of course you'll get a mail that notifies you that the build has started
12:21 JCaesar yep, that…
12:22 JCaesar "Submit" is not exactly the caption I'd give that action. ;)
12:28 larsrh JCaesar: What would you call it instead?
12:31 JCaesar "Stage for Submission" "Test build for submission" "Prepare for Submission" or so… hm.
12:32 int-e Or you could add a note ("clicking this button will initiate a test build. if that test build succeeds...; if it fails...')
12:34 int-e in the former case, I expect the request is forwarded to the afp maintainers; I have no clue what happens in the latter case
12:47 JCaesar You'll receive an email about the build status in either case.
12:47 JCaesar if it succeed, you can hit a button and it will be forwarded to the maintainers.
16:35 ammbauer noted, we'll add a note or tooltip or something.
17:49 ilbot3 joined #isabelle
17: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/

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