Stream: jsCoq

Topic: CoqDB


view this post on Zulip Karl Palmskog (Mar 18 2022 at 12:16):

yes, isn't CoqDB connected to PyCoq mainly? I thought PyCoq was the best place to expose that interface?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:17):

The design I have in mind is independent of how you access it.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:17):

It will be an OCaml program almost for sure

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:18):

PyCoq is actually, thanks to the ongoing work by Thierry Martinez just a totally automated OCaml to Python API generator

view this post on Zulip Karl Palmskog (Mar 18 2022 at 12:18):

you mean, an OCaml API?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:19):

I mean the coq-db implementation itself will likely be 100% an OCaml program

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:20):

we need to see, but in my experience anything not using OCaml for that kind of interaction with Coq is just too hard to maintain

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:20):

of course CoqDB could export the info in many formats

view this post on Zulip Karl Palmskog (Mar 18 2022 at 12:23):

why would you need it to be a standalone tool with its own exporting? If people want to use an OCaml API, they already have the choice of doing that through OCaml or Python, right?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:25):

I am not sure what do you mean Karl

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:26):

coq-db will provide functionality that is not available anywhere

view this post on Zulip Karl Palmskog (Mar 18 2022 at 12:27):

I can definitely see the need for an abstract standalone OCaml API for finding and inspecting Coq objects, which would then also be exposed via PyCoq in Python. But this is different from a program that might be run from the command line.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:27):

Yes coq-db will more of an API that a program

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:27):

I would expect people exporting the info to some graph database and interacting with the DB query language

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:27):

I don't know tho

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:27):

Don't have a clear idea on that

view this post on Zulip Karl Palmskog (Mar 18 2022 at 12:29):

right, I think the whole exporting stuff would probably fall outside the initial API. If you just define the datatypes carefully, people could write their own exporters

view this post on Zulip Emilio Jesús Gallego Arias (Mar 18 2022 at 12:31):

Yup tho at least one exported should be present from the beginning, as to validate the design

view this post on Zulip Shachar Itzhaky (Mar 19 2022 at 21:53):

Wouldn't a REST API make more sense? Then it is mostly language-agnostic. I think this is the way PyPI and NPM work.

view this post on Zulip Karl Palmskog (Mar 19 2022 at 21:55):

but there's nothing stopping you from building the REST API on top of an OCaml API? You could even use some Python web framework via PyCoq.

view this post on Zulip Shachar Itzhaky (Mar 19 2022 at 21:56):

Yeah sure, I was only suggesting that if the DB is exposed through HTTP running on some server, then users never have to "link" with the concrete implementations, instead there can be several implementations that bind it to different languages and they should be pretty thin.

view this post on Zulip Karl Palmskog (Mar 19 2022 at 22:00):

I think what Emilio is envisioning is something that is closely integrated with the OCaml side of Coq itself (possibly living in the Coq repo). Hence, it would probably hook in to Coq testing on every change of Coq. Most straightforward way to do this is by being pure OCaml.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:09):

Indeed we need to build a significant part of the core in OCAml, which is IMHO a very good idea, as using GADTs has shown that a core problem with proof assistants tooling (maintenance) is manageable.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:09):

recall that as of today, understanding Coq documents requires Coq as they can't be parsed / elaborated independently

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:10):

but yes, once the core DB functionality is there, there is no problem in exposing the API as a REST thing

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:10):

PyCoq / SerAPI are nice because they are trying to be fully automated wrappers over the OCAml API

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:11):

so you don't have to maintain that, I'd be very be nice if we could do the same for TypeScript by the way

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:12):

in fact not only nice, but necessary at some point. For now I think we have the write a Typescript type, get the OCaml version handled, but I'm more interested in the other way, as for example the notion of Coq document is canonically defined in the OCaml land

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:12):

All we are doing in a sense is CORBA/RPC XD

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:12):

that's not easy!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:13):

I have this horror movie script if some day I feel like exploring the arts, it starts with "OLE, OLE Automation, Browser Helper Object, ActiveX, COM+, DCOM, the Windows shell, DirectX, UMDF and Windows Runtime."

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:14):

Actually I never told anyone that I know how to write COM/COM+/DCOM components

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:15):

not sure what that means anymore, I should discuss with my therapist, but likely parts of my brain are still affected in a non-trivial way

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:16):

Using Windows NT 4 as my daily OS and writing COM , what kind of youth is that?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:24):

Actually I wanted to end this digression by providing a link to the classic "Type Safety in a Dynamically Extensible Class Library" but unfortunately the document seems to have banished

view this post on Zulip Karl Palmskog (Mar 20 2022 at 12:32):

Emilio Jesús Gallego Arias said:

so you don't have to maintain that, I'd be very be nice if we could do the same for TypeScript by the way

I think it would be more accurate to say: the maintenance burden for generated wrappers is manageable, and does not automatically lead to bitrot, as nearly any nontrivial intermediary API would

view this post on Zulip Karl Palmskog (Mar 20 2022 at 12:34):

if CoqDB is not in Coq's CI at minimum, it may fizzle out really quickly. Ideally, added to the Coq repo, as I already mentioned...

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:55):

Karl Palmskog said:

Emilio Jesús Gallego Arias said:

so you don't have to maintain that, I'd be very be nice if we could do the same for TypeScript by the way

I think it would be more accurate to say: the maintenance burden for generated wrappers is manageable, and does not automatically lead to bitrot, as nearly any nontrivial intermediary API would

Yes. All that I mean is the moment we have several languages we face the very old problem of typed interoperability which is still pretty hard to do well in most cases.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:55):

Karl Palmskog said:

if CoqDB is not in Coq's CI at minimum, it may fizzle out really quickly. Ideally, added to the Coq repo, as I already mentioned...

Sure, coq-db will be maintained and even why not integrated into Coq eventually

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:56):

For now we will just prototype and try to gather all related / similar purpose projects under the same roof

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:57):

But it is true that once it is working, it is a project that seems to have heavy needs of interoperability with other systems, indeed REST, Python, typescript seem like prime candidates

view this post on Zulip Karl Palmskog (Mar 20 2022 at 12:59):

REST is not really a language to me, more like a web API architecture. I assume it will then be served as JSON over HTTP?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:59):

Karl Palmskog said:

REST is not really a language to me, more like a web API architecture. I assume it then be served as JSON over HTTP?

I'm not expert, but I think it is a language in the same way "SQL" is, but I'm not sure

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 12:59):

maybe even lower level

view this post on Zulip Karl Palmskog (Mar 20 2022 at 13:00):

I mean, I have read the original REST paper/document, and that is definitely not a programming language or an implementation

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:00):

but indeed, that's an interface to Coq DB which may not be the one we will have, tho @Shachar Itzhaky point is very good in the sense that the the OCaml API exposed by CoqDB should likely be a superset of REST so we can trivially adapt

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:01):

it is an API

view this post on Zulip Karl Palmskog (Mar 20 2022 at 13:01):

I don't know what all these web types have done the last few years, but I'm sure defining REST as a language is not beyond them....

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:01):

yes you are correct

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:02):

there are two problems here, sorry I mixed them up:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:02):

they are quite orthogonal, REST is mostly concerned with 1 I guess

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:02):

tho

view this post on Zulip Karl Palmskog (Mar 20 2022 at 13:02):

you can design the OCaml API so that it becomes possible to expose it as REST via HTTP/JSON

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:02):

if REST clients are going to received objects with non trivial structure, 2 is involved as we need to provide the schema to them

view this post on Zulip Karl Palmskog (Mar 20 2022 at 13:03):

but I don't think it's very valuable to design the OCaml API to actually be like REST

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:03):

or we can just version from the start, but still, I'd be great if we could do better for the schema than manually code it, as we have been doing in JsCoq / SerAPI clients

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:04):

Karl Palmskog said:

but I don't think it's very valuable to design the OCaml API to actually be like REST

Seems like a good idea to me that some parts of it are close enough as to make it easy to expose it

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:04):

We will see what use cases coq-db wants to address

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:04):

for now the use cases I've seen are not so fancy

view this post on Zulip Karl Palmskog (Mar 20 2022 at 13:05):

how people typically treat REST is to rely on HTTP verbs like POST/PUT/DELETE. In message-passing systems, this can be considered a very poor vocabulary

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:06):

Karl Palmskog said:

how people typically treat REST is to rely on HTTP verbs like POST/PUT/DELETE. In message-passing systems, this can be considered is a very poor vocabulary

Indeed it can, not sure that is our problem tho

view this post on Zulip Karl Palmskog (Mar 20 2022 at 13:07):

if your design goal for the OCaml API is to be close to REST, I think you will probably get the forced message vocabulary paucity of most REST implementations

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:12):

Karl Palmskog said:

if your design goal for the OCaml API is to be close to REST, I think you will probably get the forced message vocabulary paucity of most REST implementations

Maybe, what is "the forced message vocabulary paucity of most REST implementations"

view this post on Zulip Karl Palmskog (Mar 20 2022 at 13:12):

one analogy: for relational databases, the query language is usually super-rich, but the data definition language tends to be limited. As for DBs, people are mostly interested in querying Coq objects, rather than removing them or updating them. Yet, REST says GET/POST/PUT/DELETE is the fundamental things everyone wants to do

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:13):

Karl Palmskog said:

one analogy: for relational databases, the query language is usually super-rich, but the data definition language tends to be limited. As for DBs, people are mostly interested in querying Coq objects, rather than removing them or updating them. Yet, REST says GET/POST/PUT/DELETE is the fundamental things everyone wants to do

Maybe, that's not so clear tho, one could imagine a use case where for example people use the coq-db to improve the documentation of theorem, provide metadata, etc... in that sense the Coq DB could update

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:13):

also the db may include some other transient metadata that is amenable to user verification

view this post on Zulip Karl Palmskog (Mar 20 2022 at 13:14):

paucity of vocabulary is just that the message types are so few (compare paucity of types)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 20 2022 at 13:19):

I see thanks! That should not be a problem IIUC, note that above I wrote "subset of the API to help REST", for sure we don't have to limit ourselves to rest


Last updated: Jan 31 2023 at 10:01 UTC