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