Ian Sweet

Results 17 comments of Ian Sweet

I'm also getting this error. OSX Version 10.14.6 Emacs Version 26.2 Coq Version 8.9.1 Proof General Version 20190821.848 Company-Coq Version 20190425.1851

I'm still having trouble with this. It seems that CAML_LD_LIBRARY_PATH was replaced with LD_LIBRARY_PATH, and this variable in master is set to: ``` export LD_LIBRARY_PATH=.:../elina_poly: ``` which is where liboptpoly.so...

The LD_LIBRARY_PATH is already set to include the directory in which liboptpoly.so resides. So I expect that even without modifying this variable, I should not get the error that I...

Off the top of my head, no. But I'm sure there is a way, and I'd be happy to look into it.

This is in the p4 directory? Just sets.cmi / sets.cmo -- is that right?

See: https://discuss.ocaml.org/t/dune-link-against-cmo-cmi-without-source/2488 Short answer: there isn't a way to do this. Long answer: is there a good reason you are doing this? If not, it'd be pretty simple to just...

I assume that the reason for not giving them the source for the canonical implementation is that you don't want it to be distributed (i.e. cheating, etc.)? Dune has support...

Actually, now that I think about it, `dune` uses `findlib` for the packages in its `(libraries ...)` clause. So, if you had a way to make the binary version of...

I think this is the best solution, because it would allow you to only distribute binaries but then also depend on them properly as a library. Although it does require...