Pass arguments from _CoqProject file to coqtop about coq-serapi

[ejgallego]

Thanks for reporting, what are the important options, paths? In this regard I plan to reuse the jsCoq package format.

I think I will add a _CoqProject parser to serapi for now, but I need to think for a couple of days.

[psteckler]

For my use case, the flags to map physical directories to logical paths is important.

[ejgallego]

@psteckler unfortunately I won't have time this week to work on this and #19.

However, SerAPI already supports the (LibAdd ($L1 ... $Ln) $path $has_ml), so you should be able to add load paths using:

(LibAdd (UniCoq) "/home/unicoq/" false)

as a substitute of Add LoadPath, but I admit it is a bit painful.

[ejgallego]

By the way SerAPI master is the right branch to use these days after EConstr.

[psteckler]

Can I just put Add LoadPath in my script, then, and not bother with command-line arguments to do the mapping? Is there any reason I can't pass Add LoadPath to SerAPI's Add?

[ejgallego]

No reason at all, that should work and I use it all the time indeed.

[psteckler]

Great, I'll try that.

[psteckler]

By the way SerAPI master is the right branch to use these days after EConstr.

Which branch of your Coq repo does that go with? Is it still stm+parsing_api, or do I now use trunk?

[ejgallego]

The current "good" combination is SerAPI trunk + Coq trunk. I hope it will stay that way for a while.

[psteckler]

Good, that's easy to remember. :-)

[ejgallego]

:D I guess I'll add a note to the README stating that for the development version .travis.yml should give you the information in the most reliable way.

[psteckler]

I just looked at the .travis.yml file.

It looks like I can just use trunk from the main Coq repo, rather than your fork, for SerAPI.

[ejgallego]

Indeed, sorry if I was not able to explain that properly. It is also highly recommended you update your findlib.conf so you can find the correct coq packages automatically for merlin.

[ejgallego]

I don't plan to support _CoqProject anymore; likely further support will come from querying Dune-enabled Coq packages, meanwhile users will have to extract -R / -Q from _CoqProject.