libera/#commonlisp - IRC Chatlog
Search
2:25:32
hayley
stylewarning: For no good reason whatsoever, here is Coq compiled to CL <https://plaster.tymoon.eu/view/3637>
2:49:58
hayley
By doing really crappy compilation of the JSON output of the Coq Extraction module. I suspect Coalton would generate much better code (mostly around munging Lisp-1/2 and FFI'ing curried functions to Lisp uncurried functions).
2:50:40
hayley
As for why, because one course this semester involves "using static analysis tools" for cloud stuffs, for which they probably mean a linter.
2:51:48
hayley
Then I had the terrible thought last night to feed verified code to CL. Not that my compiler is sound, or even close to working for anything other than ADD.
6:58:08
hayley
stylewarning: Do you have any opinions on if/how to expose curried functions to CL? I think I can glean how much to uncurry from the Coq JSON dump, but the idea of gleaning it puts me off a bit.
12:00:44
puchacz
hi, is there a lisp-to-lisp communication library that would be suitable for interactive REPL development? e.g. from SBCL sly, evaluate (with-another-lisp *abcl-connection* (do-something)) ?
12:01:41
puchacz
the reason is that my main Lisp is sbcl, but abcl has potentially access to many libraries based on java.
12:14:43
beach
You would not be able to do much with such a thing. Objects would lose their identity, and most objects would not be possible to replicate on the other side.
12:23:46
beach
Even with strings, there is not much you can do with a string such as "#<SOME-CLASS ...>"
12:25:31
puchacz
yes. only lists, actual strings, keywords, symbols used as string designators, numbers. like JSON really
13:11:42
puchacz
I wi ll have a look how it is done, but I think design goal is different - rather than have 2 lisps or more tightly coupled, sending a task to any of lisp server instances that are interchangeable
13:16:40
puchacz
systems I have in mind are like cl4py/py4cl or Rich Hickey's thingy for java<->lisp comm (was the name leaf? I can't remember now)
13:18:09
puchacz
Riich' library uses weak hash map to tell the server when it is ok to garbage collect object on java, and it either sends around self evaluating objects like strings or numbers, or creates proxies for everything on lisp side