document the *.glob file format

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4834
From: @siegebell
Reported version: unspecified
CC: coq-bugs-redist@lists.gforge.inria.fr

[coqbot]

Comment author: @siegebell

Please document the *.glob file format.

[ejgallego]

I think the *.glob file is internal and shouldn't be documented for IDE use, instead, we should export a query API for them.

[Zimmi48]

Maybe then edit the issue title and remove the kind: documentation label to reflect this, WDYT?

[ejgallego]

I am not opposed to someone writing the documentation for *.glob, I meant that it is not a priority and IDE writers should not rely on it. @siegebell 's original use case would be better served by a query API.

[Zimmi48]

OK but what I would like to understand is what you meant by the "good first issue" label: is it a good first issue to document the glob format or to export a query API for it?

[ejgallego]

To document the glob format, sorry. glob files are generated by https://github.com/coq/coq/blob/master/interp/dumpglob.ml , so I think it is pretty straightforward to extract that information.

Writing a query API requires redesign of Nametab and that looks way more complicated to me.

[Zimmi48]

Thanks for the clarification.

[cpitclaudel]

It would be very nice to have a query API for glob files. Emilio, do you already have some of that information in SerAPI?

[ejgallego]

@cpitclaudel there is some information indeed that can be already accessed, the rest should be easy. glob is slightly awkward in the sense that it is fully ad-hoc.

I am working on a new setup that should provide pretty good query capabilities [and my schedule is finally freeing so expect to do progress soon], but meanwhile, if you open an issue for SerAPI I'm sure we can easily add many things.

Additionally there is hope we get someone to work on improving the glob format.

A particular problem to take into account is that Coq tends to store the same information in different layers, and with different semantics; usually you have at least:

• the kernel environment, which contains all the logical definitions, in kernel format
• the libobject, which contains scope-aware definitions in several formats
• the Nametab, which contains important information regarding name resolution.
• quite a bit of here-and-there state, such as notations or parsing
• the STM, which contains a hybrid of document/schedule in its vcs tree.

glob information is not derived from any of those, but globally dumped by interleaving calls in different codepaths.

[MSoegtropIMC]

So what is the proposed solution for doc2html? Since tools using .glob already exist I am not sure an API would be appreciated.

[xavierleroy]

Recent Github activity points me to this issue report, which I hadn't seen before.

My own coq2html tool would very much benefit from a specification of the .glob file format, kept up to date as it evolves.

I'm not interested in an API, for two reasons. First, the .glob file format is line-oriented and trivial to parse using regexps or ocamllex lexers. What's not easy is to understand the meaning of the various fields. Second, coq2html today is a single source file with zero dependencies, and I'd rather keep it like this than link with a big API and its boatload of dependencies.

[ejgallego]

My own coq2html tool would very much benefit from a specification of the .glob file format, kept up to date as it evolves.

Hi @xavierleroy , see #14966 ; could you have a look and see if that would suffice?

I'm not interested in an API, for two reasons. First, the .glob file format is line-oriented and trivial to parse using regexps or ocamllex lexers. What's not easy is to understand the meaning of the various fields. Second, coq2html today is a single source file with zero dependencies, and I'd rather keep it like this than link with a big API and its boatload of dependencies.

Actually one of the reasons this format has not evolved at all is that the current implementation and format is a mess; moreover, there is no way to use the type system for example to be sure that coqdoc and coq2html are in sync would we evolve the format. One more reason for the not very exciting status of Coq libraries documentation.

Specifying the format a an OCaml data type is, IMHO, superior in every possible way [and allows to have a clear upgrade path, etc...] Moreover, good semantic information cannot be just encoded this way, UIANM (*)

But you are correct that documenting the format takes a few mins and it is benefitial for users of it.

IMVHO the "single source file with zero deps" argument is a bit weak these days too, it takes 3 lines to do a build definition such as

(executable
  (name coq2html)
  (libraries coq-core.glob))

and you get a lot of other benefits such as integration with dune-release, etc...

(*) Actually we almost got ready a replacement for .glob that I'm sure will be more pleasant to work with and provide many more features such as implicits, etc...