Stream: Elpi users & devs

Topic: ELPI Hacks

Philip (Sep 26 2023 at 10:39):

Do I understand correctly that the Hacks "readterm" and "string_to_term" are not usable from within Coq-ELPI?

Enrico Tassi (Sep 26 2023 at 11:02):

I may have not enabled them, and I'm fine doing it now since I understand your use case.

Look here and add the corresponding set of builtins: https://github.com/LPCIC/coq-elpi/blob/dfe528598d04588376eb6b240003647cdd5aa473/src/coq_elpi_programs.ml#L255-L266

Enrico Tassi (Sep 26 2023 at 11:03):

But IIRC we found a way around it, no?
Like generating an external file and then Elpi Accumulate it.

Philip (Sep 26 2023 at 13:37):

That would be an alternative, but not having to write out a file (which ideally should happen in some temporary directory, that has to be located in a platform-dependent way), seems like more of a headache if in my case reading in the standard-output of a process is just as viable, assuming there is no reason that you decided not to enable readterm.

Enrico Tassi (Sep 26 2023 at 14:07):

The problem is that readterm only makes sense in the empty context, since the "parser" does not know the context. This is why I document it as an hack.

Philip (Sep 27 2023 at 09:16):

I was thinking about readterm analogously to Lisp's read; am I mistaken in doing so?

Philip (Sep 28 2023 at 08:42):

Enrico Tassi said:

I may have not enabled them, and I'm fine doing it now since I understand your use case.

Look here and add the corresponding set of builtins: https://github.com/LPCIC/coq-elpi/blob/dfe528598d04588376eb6b240003647cdd5aa473/src/coq_elpi_programs.ml#L255-L266

Do you think it would make more sense to add lp_builtins to that list, or to move string_to_term and readterm to io_builtins? The latter would seem to complement term_to_stringbeing part of io_builtins.

Enrico Tassi (Sep 28 2023 at 09:08):

I suggest adding lp_builtins. I prefer to keep that stuff in the "lambda prolog specific" set of builtins, as I was saying they are problematic (implemented to run existing lp code only), while the other io_builtins are OK IMO.

The fact that you have a use case for them does not mean we can't do better. For example these builtins don't even typecheck the term read, they are a bit unsafe (as OCaml's Marshal module is). I don't think you can really crash elpi, but they are still problematic IMO.

Philip (Sep 28 2023 at 09:31):

Ok, these changes appeared to run through cleanly on my end: https://github.com/LPCIC/coq-elpi/pull/506.

Last updated: Oct 13 2024 at 01:02 UTC