Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-04-04

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

All times shown according to UTC.

Time Nick Message
01:04 fracting1 joined #isabelle
01:37 fracting1 joined #isabelle
01:40 fracting1 joined #isabelle
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/
05:20 fracting joined #isabelle
05:22 fracting joined #isabelle
05:25 fracting joined #isabelle
09:22 JCaesar Is there an equivalent to apply(rule_tac x = None in exI) for the type of goal that is generated by obtain?
09:23 larsrh It's called Isar ...
09:24 larsrh No need to use rule_tac in this case, btw, because "None" does not contain bound variables
09:24 larsrh apply (rule exI[where x = None]) is the slightly less improper way of doing it
09:24 larsrh If you really want to continue using apply scripts, try apply (atomize_elim, rule exI...)
09:29 JCaesar Isar it is…
09:30 JCaesar I just feel like obtain goals aren't the most beautiful thing in isar…
09:54 larsrh I tend to agree.
10:03 ThreeOfEight I occasionally use "apply (auto intro!: bexI[of _ i])"
10:03 ThreeOfEight don't judge
10:24 int-e been there
10:26 int-e (auto intro!: exI[of _ "E (k mod length X)"] exI[of _ 0] ...)
10:58 Damaki joined #isabelle
14:33 chuchucorny is there a way to add a meaningful error message to exported haskell code when I use undefined in Isabelle?
14:35 chuchucorny For example, if "foo x" is only defined if "P x" holds, I like to wrap my exported code inte "if P x then foo x else undefined" to avoid calling foo without the necessary precondition. However, if the haskell program aborts with "undefined", it is almost impossible to find out which undefined triggered
14:44 larsrh consts mybetterundefined :: "'a"
14:44 larsrh declare [[code abort: mybetterundefined]]
14:44 larsrh export_code mybetterundefined in Haskell
14:44 larsrh This will use Haskell's built-in "error" function, but with a string telling which function it was thrown from
14:46 chuchucorny the consts sounds dangerous. Is there a way to just modify the haskell code?
14:47 larsrh Why does it sound dangerous?
14:47 larsrh You're declaring an uninterpreted constant
14:48 larsrh *unspecified
14:49 chuchucorny hmm, undefined is an axiomatization
14:49 larsrh Albeit without any actual axioms
14:49 larsrh The purpose of this is to 'conceal' the constant, i.e., nobody should be able to define "undefined = 42"
14:51 chuchucorny so defining consts for every "exception" is perfectly safe?
14:51 larsrh sure
14:51 chuchucorny is it also beautiful?
14:52 larsrh As beautiful as generated code gets.
14:53 chuchucorny okay
15:05 chuchucorny thanks
15:15 JCaesar To get real error messages, you'd need some code printing setup for those constants though, right?
15:16 ThreeOfEight What do you mean by "real error message"?
15:17 chuchucorny a string for example
15:17 chuchucorny not some undefined_here_be_my_error_message
15:18 JCaesar ThreeOfEight: Something you'd not be afraid to showing a user that has no idea what Isabelle or Haskell is.
15:19 larsrh JCaesar: Don't use Haskell pure exceptions, then
15:20 chuchucorny wrapping everything into None is quite ugly, the exception should only trigger if the function's api is misused
15:22 larsrh Use the monads!
15:24 chuchucorny let me think about this
15:27 JCaesar Option.bind_splits ftw.
15:27 JCaesar There's no ErrorMonad though, is there?
15:36 larsrh JCaesar: 'a + 'b
15:36 JCaesar Has that been made a Monad?
15:38 JCaesar I'd love to have that.
15:38 larsrh Not sure. Either way, it's trivial
16:53 ThreeOfEight JCaesar/chuchucorny: ideally, you should have code around your API checking all preconditions so that no errors can occur
16:53 ThreeOfEight that code can be verified or unverified
17:06 JCaesar so you may deny a few inputs unnecessarily or accet a few and get ugly error message.
17:06 JCaesar *messages
17:06 JCaesar Hm.
17:06 JCaesar Generally yes. I have one case though where a "this cannot be done at this size and shape of data" occurs. There's really no easy way to predict when…
18:41 dmiles_afk joined #isabelle
19:05 Damaki joined #isabelle

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