Camelia, the Perl 6 bug

IRC log for #darcs, 2013-02-27

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

All times shown according to UTC.

Time Nick Message
00:06 preflex joined #darcs
01:59 mizu_no_oto joined #darcs
02:26 lambdabot joined #darcs
02:29 mizu_no_oto joined #darcs
02:30 intripoon_ joined #darcs
02:32 lambdabot joined #darcs
02:41 mizu_no_oto joined #darcs
02:43 mizu_no_oto joined #darcs
03:15 intripoon joined #darcs
03:16 mizu_no_oto joined #darcs
03:35 mizu_no_oto joined #darcs
03:55 xymox joined #darcs
03:56 xymox joined #darcs
04:10 mizu_no_oto joined #darcs
04:38 preflex_ joined #darcs
06:47 favonia joined #darcs
06:49 lelit joined #darcs
08:21 raichoo joined #darcs
08:23 amgarchIn9 joined #darcs
09:33 florent_ joined #darcs
09:34 gal_bolle hi al
09:34 gal_bolle and all other too
09:37 florent_ joined #darcs
10:30 gal_bolle is it possible to obliterate patches on darcshub?
10:35 iago joined #darcs
11:25 iago joined #darcs
11:41 iago patches suspended by rebase are not completely invisible, at least not for "changes" and "diff", darcs diff -n 0-1 for instance
11:42 owst joined #darcs
11:42 iago not sure if I should report this as a bug
11:43 iago I would expected --index to skip suspended patches, as if they didn't exist
11:43 owst What is --index?
11:44 owst (I might have joined in the middle of a conversation)
11:44 owst gal_bolle: yes it is possible
11:45 owst ssh user@hub.darcs.net oblit REPONAME
11:49 iago owst, the --index option for changes for instance
11:49 iago I think you just missed this: «patches suspended by rebase are not completely invisible, at least not for "changes" and "diff", darcs diff -n 0-1 for instance»
11:51 owst Oh, iago I was getting confused by what --index did
11:51 owst Yes, I think that's a bug in the tracker (I believe I hit the same issue)
11:52 owst iago: not exactly, but this is the same root cause I imagine http://bugs.darcs.net/issue2260
11:59 iago Yep, they (probably) share the same cause. «It's a point against the "rebase as a patch" design.» <-- I agree
12:00 iago not sure what drawbacks are associated with having a separate stack of suspended patches
12:07 owst I think Heffalump told me once, but I don't recall. Maybe if he turns up, we can write whatever he says on the wiki (assuming it's not there already)
12:08 owst Well after a quick search, I can't see anything on the BTS
12:16 stepkut joined #darcs
12:27 * Heffalump appears
12:27 Heffalump what's the question?
12:28 Heffalump owst: are you going to reply about darcshub/github on the list (you might already have done so, my email downloading is being very slow)
12:30 Heffalump if the question is about why the suspended patch, it's documented in Darcs.Patch.Rebase Note [rRebase representation]
12:31 Heffalump roughly speaking I didn't feel confident of maintaining data integrity with the current state of the repository code
12:32 Heffalump and it's generally quite hard to make the repository code witness-safe (independent of its current shnky nature) because it represents a state on disk
12:32 * owst goes for lunch wonder which email Heffalump means
12:33 Heffalump Ash Moran's one
12:33 owst On darcs-users?
12:33 * owst is gone
12:33 Heffalump ' Best way to sync darcs / Darcs Hub -> git / GitHub?'
12:33 Heffalump yes
12:34 donri joined #darcs
13:26 gh_ joined #darcs
13:29 mizu_no_oto joined #darcs
13:47 iago Heffalump, if the main problem are witnesses then it is unlikely to change I guess, even if you make it more robust it will continue to be imperative in its nature
13:47 iago (talking about repository code)
13:48 iago I don't think that witnesses are so important, since they basically caught a very specific class of bugs
13:48 iago but that's my opinion
13:51 iago I relied myself on type hackery for my thesis and it only made me against them
14:03 * owst returns, but doesn't seem to see any hub-like emails from Ash Moran to darcs-users
14:07 Heffalump iago: they also allow you to program without tinking about that class of bugs
14:07 Heffalump which for me is the real win
14:07 owst Yes, definitely.
14:09 owst I wonder how plausable it would be to customise the errors you get when a skolem variable escapes, or you try and :>: wrong patches?
14:09 owst "Urk: you've unsealed a patch that we don't know anything about, it's not safe to use it elsewhere"
14:09 iago True. But it tends to require plenty of workarounds to keep the program well-typed. Changes that would require very little effort may require enough refactoring to drive you crazy. In my case I had to live with that, but in more stable code bases that will basically prevent some changes. In fact, I think kowey posted some though about that in G+.
14:10 owst iago: can you give an example? (I've probably not done enough patch-level stuff to think of one)
14:11 iago owst, I cannot easily talk about the Darcs case, it is just my experience with abusing the type system
14:11 Heffalump there's always the unsafeCoerce escape
14:12 iago in my case I decided to make an AST dependent of the compilation phase
14:12 iago it turned out to be a hell
14:12 * owst doesn't understand. Dependent how?
14:12 Heffalump owst: http://lists.osuosl.org/pipermail/da​rcs-users/2013-February/026799.html
14:13 iago AST Pr -> The AST after parsing, AST Tc -> the AST after typechecking, and so on
14:13 iago instead of AST id I just had a type-family from phase to type-of-identifiers-for-that-phase
14:14 iago for example
14:14 owst Ah, gotcha, thanks Heffalump
14:14 owst (stuck in a spam filter)
14:16 iago don't know, testing looks much cheaper
14:17 owst as long as you test for the right things...
14:17 iago I still use type hackery sometimes, but I think it twice
14:17 iago or three times
14:17 iago owst, the same argument is applied to type witnesses, isn't it?
14:19 owst You said testing is cheaper; I'd suggest it's only cheaper *and* as good as being type-correct with witnesses, if you have a large number of tests to ensure you never reach a bad state (even internally)
14:19 owst that said, I understand the argument against fancier types
14:19 owst hey, let's all just move to coq and be done with it :-p
14:20 iago well, Tony Hoare said "assert early, assert often"
14:20 owst If your code doesn't compile, that's an early assert as you can get ;-)
14:21 owst s/an early/as early an/
14:21 iago owst, I'm not against types, otherwise I would be using python :P
14:21 iago I simply accept the limits of type checking as an automated & painless method for catching errors
14:22 owst heh
14:22 owst Automated & painless, together, that's the problem
14:22 Heffalump and type witnesses are just one point further on from not having them - they don't model everything
14:22 iago to compare testing vs type witnesses then we should focus on the specific class of errors caught by witnesses
14:23 iago and be aware of those unsafeCoerceS that are not type safe at all
14:23 owst I wonder how far you could get with a dependently-typed patch theory
14:23 Heffalump the class being "patches used in their wrong context"
14:24 owst the type of valid hunks depends on the "current" contents of the file
14:25 mizu_no_oto joined #darcs
14:25 iago Heffalump, you can test about that using RepoModel, don't you?
14:26 Heffalump iago: not very well
14:26 Heffalump mostly patches work fine in the wrong context
14:26 Heffalump also, the compiler is much faster than th  unit tests :-)
14:28 owst as long as you don't compile everything 3 times :-p
14:28 iago well, I won't use the term "wrong context" for a context in which a patch can be applied successfully
14:28 iago but I understand that sometimes some patch manipulation is more restrictive than that
14:29 Heffalump it might for example succeed but produce the wrong result
14:29 iago but you usually have a sequence of patches
14:30 iago ps --> ps'
14:30 iago I would be surprised in some bug in the process won't cause so p_i to fail
14:30 iago s/so p_i/some p_i
14:31 iago anyway, as always, there is no definitive choice
14:31 iago for me is more important being able to change things easier
14:32 iago it would be necessary a master thesis on testing Darcs to compare both :P
14:33 iago to see how many bugs catch each one
14:34 owst How do you count bugs that never appear, since the type system disallows code that would introduce them?
14:36 iago I ask you to write down whenever type witnesses prevents a bug
14:37 owst SOunds tricky to me ;-)
14:37 iago owst, how do you count bugs that were not introduced because a test case failed?
14:38 owst I don't know, you suggested that this count was useful/doable!
14:38 iago I wasn't trying to be 100% accurate lol
14:38 iago lispy reported some errors after introducing type witnesses, it would be interesting having an analogous report for testing
14:39 owst I think both have their place in the darcs codebase
14:39 owst (testing/witness-stuff)
14:39 iago do you think that having both data would be useless?
14:40 iago anyway I could say you that standards for safety critical software do not rely on type hackery
14:40 owst I don't think it would be useless. I think it might be hard to infer much from it, and I'm certainly not going to try and collect the data :-)
14:40 iago and it's probably the most reliable software you can find
14:40 iago even when written in C
14:41 owst iago: perhaps, but focussed attention by whatever means (designing complicated types, or thorough test suites) is likely to give good software
14:41 iago how do you support that argument?
14:41 owst I don't.
14:42 iago there is evidence for testing
14:42 iago I don't know of too much evidence for type witnesses
14:42 iago :-P
14:42 owst sure, testing is more established, and easier.
14:43 iago to be fair we should also mention other techniques for bug finding
14:45 iago I must said I don't want to be misunderstood, it's more a question of where we put the line, when type systems are more painful than helpful
14:46 iago I don't have the *answer*, but testing should not be underestimated
15:17 gbeshers joined #darcs
15:33 mizu_no_oto joined #darcs
17:34 lispy on the topic of tests/witnesses/etc, has anyone considered using liquid haskell on the darcs source?
17:35 lispy (note: I don't really think adding new forms of correctness testing should be a high priority, more just curious if anyone has considered liquid haskell for darcs)
17:38 Heffalump no, but in theory I'd like to
17:39 Heffalump iagsafety critical software is also extremely expensive to devleop (but you're not here :-)
18:04 owst iagdamnhesnothereautocompletefail
18:06 lispy Heffalump: Sometimes I think I'm just looking for an excuse to play with neat tools
18:07 lispy Heffalump: I've been trying to convince someone to make a lambdabot plugin that lets folks play with liquid haskell
18:08 mizu_no_oto joined #darcs
18:16 Heffalump owst: that's the problem with typing blind on a laggy cnonection :-)
19:25 raichoo joined #darcs
19:44 amgarchIn9 joined #darcs
20:09 mizu_no_oto joined #darcs
20:19 favonia joined #darcs
20:29 carter_ joined #darcs
20:40 sm_ joined #darcs
22:09 favonia joined #darcs
22:09 mizu_no_oto joined #darcs
22:30 favonia joined #darcs
22:33 carter joined #darcs

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