Li-yao (Apr 04 2024 at 16:44): Li-yao (Apr 04 2024 at 16:44):How do you define a bunch of functions that you can reuse between different commands? Db and File? Both are a bit inconvenient, File because of having to change files, and Db because it doesn't use the same Accumulate syntax as Command (db must be named, so I can't just copy-paste a sequence of Accumulate blocks).
I naively thought I could reuse stuff in an Elpi Program but beyond the tutorial I don't see any documentation on what Program actually does.
Enrico Tassi (Apr 04 2024 at 20:08):I would recommend using files. What is the disadvantage you see? No feedback when you hover on {{ coq code }}?
Db also work (I don't fully understand your copy/paste problem, note that in 2.1.0 there is a new syntax for accumulation). But Dbs are really designed to be extended programmatically, using them to share "static" code may work but it is not intended.
All in all, I'd like to understand what is the exact problem and provide a solution. An Elpi Program is just a command with no pre-loaded code. So it could as well become a thing, like a file, you can reuse in multiple commands. But first I need to understand what is the problem with files ;-)
Li-yao (Apr 04 2024 at 20:24):Maybe I just need to get used to working with elpi files. I don't have a big development yet, so I liked having it all in a single file with small Accumulate chunks so I can experiment interactively in the middle of my development. I don't even have editor (vim) support for elpi yet.
Enrico Tassi (Apr 04 2024 at 21:10):I see. I had some vim instructions in the elpi readme, maybe check the file history
Last updated: Oct 13 2024 at 01:02 UTC