01:13 (quit) asumu: Read error: Connection reset by peer
01:29 (quit) jeapostrophe: Quit: jeapostrophe
02:04 (quit) Rakko: Quit: Rakko
02:25 (join) samth
02:32 (quit) jonrafkind: Ping timeout: 276 seconds
02:40 (quit) samth: Ping timeout: 265 seconds
03:28 (join) samth
03:38 (join) martin_hex
03:38 (quit) martinhex: Disconnected by services
03:38 (nick) martin_hex -> martinhex
03:49 (join) rbarraud
03:58 (join) rbarraud_
03:58 eli: samth: re the "sharp edges" from earlier, combining `dynamic-require' with `define-runtime-path' should make sure there are no problems.
03:59 (quit) rbarraud: Ping timeout: 260 seconds
03:59 (part) eli: "rcirc on GNU Emacs 23.1.1"
03:59 (join) eli
04:00 samth: eli, the dynamic-requires are all to collection paths
04:01 samth: ie (dynamic-require 'typed-scheme/foo 'bar)
04:01 samth: so no need for define-runtime-path
04:01 eli: That's irrelevant.  It might be that some dependency is lost, still.
04:02 samth: i'm confused then - what runtime path do you want me to use?
04:03 eli: The thing is that if you have (dynamic-require whatever), there is no way to statically tell that you depend on anything.
04:04 eli: `define-runtime-path' is a way to register dependencies on files without requiring them.
04:04 samth: ah, i see
04:04 samth: i don't want to have a `define-runtime-path' specifying all of the TR impl, though
04:04 eli: So `dynamic-require' + `define-runtime-path' might be a good combination for avoiding any distribution issues, and also avoiding the module loading problem.
04:04 samth: since that's something like 100 files
04:05 eli: You don't need everything, just each required file.
04:05 eli: (dynamically-required)
04:05 eli: You could probably lump it into a macro, somehow.
04:06 samth: but the distribution mechanism doesn't follow requries from a path in `define-runtime-path'
04:06 eli: (BTW, my guess is that Matthew isn't worried about racket distribution -- but about distributing executables, which uses these dependencies.)
04:06 samth: so if I add (define-runtime-path "core.rkt") and core.rkt requires "private/bar.rkt", the executable generator won't follow the second link
04:07 eli: The distribution mechanism -- both racket and executables -- recurs down the dependency graph, which you get via both `require' and `define-runtime-path'.  So the end result will be the same in both.
04:07 eli: It should.
04:07 eli: Let me check something.
04:07 samth: that would be very surprising, since `define-runtime-path' specifies data, not code, in general
04:08 eli: (Sorry, slow machine -- the nightly build is running now.)
04:14 eli: samth: using it (`define-runtime-path') doesn't record the dependency in the .dep file -- I'm not sure whether this is broken or if the dep files don't record these things.
04:14 samth: i don't think `define-runtime-path' is supposed to do that sort of thing
04:15 eli: This means that the racket distribution won't see those dependencies.
04:15 eli: But the executable creating process definitely should.
04:15 eli: So the only question is whether a `define-runtime-path' dependency on a module will drag in its dependencies too.
04:16 samth: i'd be really surprised if it did
04:16 eli: Alternatively, it might take the whole directory in if you use `define-runtime-path' with the whole directory.
04:16 eli: (Something like (define-runtime-path here "."))
04:16 eli: I'd be surprised if it didn't, btw.
04:17 eli: (But that's not my code, so I don't really know.)
04:19 samth: eli: Use define-runtime-module-path to bind a module path that is passed to a reflective function like dynamic-require while also creating a module dependency for building and distributing executables.
04:19 samth: from the docs
04:20 samth: however, i don't want that dependency
04:21 eli: samth: Ah, I thought that there was something like that.
04:21 eli: That sounds exactly like what you want.
04:22 eli: It's not a dependency in any *-time, only for those things.
04:22 eli: And you do want distributed TR programs to still be compilable.
04:23 samth: TR *programs* will be distributable
04:23 samth: TR *itself* won't be
04:23 samth: `for-label' still has overhead - I want 0 overhead
04:24 eli: That `define-runtime-module-path' is not a `for-label' require.
04:24 samth: yes, it is
04:24 samth: The define-runtime-module-path form creates a for-label dependency from an enclosing module to module-path.
04:24 samth: (from the docs)
04:25 eli: In that case, "ugh".
04:26 eli: samth: Seems like what I thought it was doing is what you really want.  Having it do a `for-label' require seems like a bad idea, given that it's not the same.
04:26 eli: I'd complain.
04:26 samth: once i have something working using dynamic-require as much as possible, i'll talk to matthew
04:27 samth: but i'm making progress on that
04:27 samth: current master loads about 200 modules for any TR file, i've got it down to 150, and i should be able to get it down below 50
04:28 eli: Is there any need for anything, except for contracts?
04:32 samth: there are a few other things that are in the residual program
04:33 samth: but the hard-to-remove parts are the dependencies of typed-scheme/private/base-types
04:33 samth: you can see my discussion w/ ryan above about that
04:34 samth: search for make-a-type
04:38 eli: samth: Why is `type-table' in the runtime?
04:40 samth: it's not
04:41 samth: oh, my code snippet was wrong, it should be (begin-for-syntax (dict-set! ...))
04:41 eli: Ah.
04:42 eli: In this case, the whole `dict-set!' can be done via a syntax-time `dynamic-require' too, no?
04:45 samth: well, that would be nice
04:45 samth: but it's not obvious how
04:46 samth: what module would be dynamic-required?
04:47 eli: "A magical one"?
04:47 eli: But I see the problem.
04:48 eli: Maybe turn that make-a-type thing into a dynamically required functionality,
04:48 eli: which means that you only construct descriptions of types, not the actual types.
04:56 samth: yeah, all the solutions i've thought of involve eval or the moral equivalent
04:56 samth: i'd like to do this without making the compile-time portion of TR slower
05:09 (join) spidermario
06:10 (quit) samth: Ping timeout: 240 seconds
08:04 (join) hanDerPeder
08:04 (quit) rbarraud_: Ping timeout: 240 seconds
08:17 (quit) tcoppi: Ping timeout: 240 seconds
08:18 (join) tcoppi
08:43 (join) jeapostrophe
08:50 (join) b-man_
08:54 (part) kukka
09:03 (join) hellmage
09:24 (join) asumu
10:26 (join) sstrickl
10:29 (quit) asumu: Read error: Connection reset by peer
10:52 (join) martin_hex
10:52 (quit) martinhex: Read error: Connection reset by peer
10:52 (nick) martin_hex -> martinhex
10:58 (quit) jeapostrophe: Quit: jeapostrophe
11:04 (quit) hanDerPeder: Remote host closed the connection
11:04 (join) hanDerPeder
11:09 (join) jonrafkind
11:36 (quit) uygur: Quit: Page closed
12:04 (join) asumu
12:23 (join) carleastlund
12:30 (quit) eli: Ping timeout: 264 seconds
12:46 (quit) hanDerPeder: Quit: hanDerPeder
12:46 (join) eli
12:57 (quit) hellmage: Ping timeout: 252 seconds
13:09 (join) anRch
13:18 Lajla: I have learnt syntax case. \o/
13:18 Lajla: jonrafkind, hug me
13:18 jonrafkind: now you have to learn syntax parse
13:18 jonrafkind: syntax case is obsolete!
13:19 (join) samth
13:24 clklein: Yeah, soooo 90s
13:25 (quit) samth: Ping timeout: 260 seconds
13:49 (quit) asumu: Ping timeout: 265 seconds
14:04 (quit) spidermario: Remote host closed the connection
14:10 (quit) anRch: Ping timeout: 276 seconds
14:16 (join) anRch
14:28 (quit) anRch: Quit: anRch
15:14 jonrafkind: clklein, I used `generate-term' for your STLC language and it generated: '(λ (C : (→ (→ Num (→ Num Num)) (→ (→ (→ Num (→ Num Num)) (→ Num (→ Num Num))) (→ Num (→ Num Num))))) (λ (T : Num) g))
15:15 jonrafkind: which I think has a few problems..
15:15 jay-mccarthy: such as?
15:15 jonrafkind: well g is a free vairable
15:15 jay-mccarthy: generate-term generate parseable terms
15:15 jay-mccarthy: not type checked or error checked terms
15:15 jonrafkind: oh actually I guess im not running the typecheck metafunction on it
15:16 jonrafkind: i guess i need a where clause in my pattern or something
15:20 clklein: I wouldn't try to put typedness into a side-condition pattern (although there's nothing stopping you).
15:20 jonrafkind: well can I use redex-check with a has-type? property?
15:21 jay-mccarthy: i think he's doing in the condition on generate-term/redex check
15:21 jonrafkind: (redex-check STLC (λ (x : τ) e) (has-type? e))
15:21 jay-mccarthy: not in the reductions
15:21 clklein: instead just test properties with the shape (λ (t) (or (well-typed? t) (good? t)))
15:21 jay-mccarthy: and
15:22 jonrafkind: whats good?
15:22 jay-mccarthy: the "real" property
15:22 jonrafkind: oh oh right
15:22 clklein: The thing that should hold for well-typed terms.
15:22 jay-mccarthy: warning: most terms it will generate will not be well typed
15:22 jonrafkind: how do I use the has-type? metafunction
15:23 jay-mccarthy: (in my experience)
15:23 clklein: oops, i meessed that up. I meant (not (well-typed? t))
15:23 jonrafkind: jay-mccarthy, yes im testing how bad redex-check is
15:23 jay-mccarthy: call metafunctions with (term (meta ,racket-id))
15:28 jonrafkind: (redex-check STLC (λ (x : τ) e) (lambda (e) (error 'failed "failure")))
15:28 jonrafkind: it doesnt seem to matter what i type for the property.. it just says "no counter examples found in 1000 attempts"
15:30 clklein: redex-check's third position isn't supposed to be a procedure
15:30 jonrafkind: oh oops
15:30 jonrafkind: i thought thats what you meant by (λ (t) (or (well-typed? t) (good? t)))
15:30 clklein: Everyone seems to do that.
15:31 clklein: Oh, yea, that was a misleading explanation :)
15:32 jonrafkind: urgh, the dreaded 'bad syntax' error. clklein, can you add a better error message to redex-check?
15:32 jonrafkind: (redex-check STLC ((λ (x : τ) e) (not (term (has-type? e)))))
15:34 clklein: ok
15:34 jonrafkind: (redex-check STLC (λ (x : τ) e) (not (term (has-type? e)))) ;; shoulndt this find well-typed terms?
15:36 clklein: It's testing the claim that no lambda term has a type. A counterexample is one that does have a type, so yes, it should. Is it doing something else?
15:37 clklein: Oh, wait, no it's not. You're checking that the body does not have a type, not the whole lambda
15:38 clklein: You probably want to replace the pattern in the second position with just e
15:38 jonrafkind: ok, but i want to force that the whole term is at least a lambda
15:38 jonrafkind: otherwise it will generate simple things like '1'
15:39 jonrafkind: can I name the whole pattern?
15:39 jonrafkind: oh i can just pass the whole thing off to has-type? i guess
15:39 clklein: There is a pattern (name id pattern) you can use
15:40 clklein: (name e (λ (x : τ) e_0))
15:41 jonrafkind: ok
15:41 clklein: But you can also reconstruct the term in the property, as you realized
15:43 jonrafkind: ok it only takes about 80 tries to generate a well-typed term
15:43 (join) drhodes_
15:44 clklein: Really? It finds one on its first try every time for me.
15:44 clklein: (λ (x : Num) 0)
15:45 jonrafkind: you mean after 0 attempts?
15:45 clklein: after 1 attempt
15:45 jonrafkind: i changed my pattern to (e_1 e_2)
15:45 jonrafkind: can I make redex-check find more than 1 counter-example?
15:46 clklein: No, but you can hack it. I'll show you.
15:46 jonrafkind: you will learn by the numbers, i will teach you!!
15:47 (quit) drhodes: Remote host closed the connection
15:47 clklein: :)
15:50 lisppaste: clklein pasted "you will learn by the numbers, i will teach you!!" at http://paste.lisp.org/display/114164
15:52 jonrafkind: so what makes this execute more than once
15:53 jonrafkind: and why wouldnt it just keep finding the same terms repeatedly
15:54 jonrafkind: ok well it produced a lot of stuff
15:54 clklein: Sorry, didn't use enough numbers... the property is always true because it returns void. I shouldn't have done that.
15:57 jonrafkind: i guess it works
15:57 jonrafkind: it would be nice to force it to generate more interesting terms
15:58 clklein: I agree.
15:58 clklein: But for now, I just let it run longer than necessary.
15:59 jonrafkind: it seems one issue is that for number it generates any number instead of just 1, so (lambda (x) 1) is different from (lambda (x) 4)
15:59 jonrafkind: and I added a string type, so now it can generate lots of redundant stuff
15:59 jonrafkind: can I restrict n to just 1 ?
16:00 jonrafkind: apparently so..
16:00 clklein: Change the definition of n.
16:01 jonrafkind: so this seems ok to me, it generates well-typed terms with reasonable efficiency
16:01 jonrafkind: so you dont think we can use this to generate agda terms and try to check them?
16:03 clklein: It's worth a shot, but as you noticed, it's pretty braindead.
16:05 clklein: (worth a shot because it shouldn't be too much work to try it)
16:09 (join) acon
16:14 (join) _ryanc_
16:39 (join) rbarraud_
16:48 (quit) acon: Quit: acon
17:06 (quit) sstrickl: Quit: sstrickl
17:07 (join) acon
17:08 (join) acon_
17:12 (quit) acon: Ping timeout: 245 seconds
17:12 (nick) acon_ -> acon
17:20 (quit) acon: Quit: acon
17:57 (join) samth
18:03 (join) jeapostrophe
18:04 (quit) jeapostrophe: Client Quit
19:18 (quit) _ryanc_: Quit: Leaving
19:29 (quit) drhodes_: Quit: leaving
19:46 (quit) jao: Ping timeout: 265 seconds
19:51 (join) jao
20:04 (join) Spewns
20:35 (quit) jonrafkind: Ping timeout: 255 seconds
20:44 (join) jeapostrophe
20:46 (quit) carleastlund: Quit: carleastlund
20:50 (quit) evhan: Ping timeout: 276 seconds
20:50 (join) evhan
20:50 (quit) jeapostrophe: Quit: jeapostrophe
20:53 (quit) Spewns: Quit: Leaving.
21:00 (quit) samth: Ping timeout: 252 seconds
21:06 (quit) evhan: Ping timeout: 255 seconds
21:07 (join) evhan
21:11 (quit) b-man_: Remote host closed the connection
21:13 (quit) evhan: Ping timeout: 245 seconds
21:15 (join) evhan
21:20 (join) hellmage
21:27 (join) hanDerPeder
21:31 (quit) hellmage: Ping timeout: 240 seconds
22:02 (quit) hanDerPeder: Quit: hanDerPeder
22:18 (join) asumu
22:23 (join) hellmage
23:29 (quit) asumu: *.net *.split
23:37 (join) asumu
23:59 (join) jeapostrophe