CoqDB · jsCoq · Zulip Chat Archive

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?

Emilio Jesús Gallego Arias (Mar 18 2022 at 12:25):

I am not sure what do you mean Karl

Emilio Jesús Gallego Arias (Mar 18 2022 at 12:26):

coq-db will provide functionality that is not available anywhere

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.

Emilio Jesús Gallego Arias (Mar 18 2022 at 12:27):

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

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

Emilio Jesús Gallego Arias (Mar 18 2022 at 12:27):

I don't know tho

Emilio Jesús Gallego Arias (Mar 18 2022 at 12:27):

Don't have a clear idea on that

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

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

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.

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.

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.

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.

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.

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

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

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

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

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

Emilio Jesús Gallego Arias (Mar 20 2022 at 12:12):

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

Emilio Jesús Gallego Arias (Mar 20 2022 at 12:12):

that's not easy!

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."

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

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

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?

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

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

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...

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.

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

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

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

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?

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

Emilio Jesús Gallego Arias (Mar 20 2022 at 12:59):

maybe even lower level

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

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

Emilio Jesús Gallego Arias (Mar 20 2022 at 13:01):

it is an API

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....

Emilio Jesús Gallego Arias (Mar 20 2022 at 13:01):

yes you are correct

Emilio Jesús Gallego Arias (Mar 20 2022 at 13:02):

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

API definition
exposing the API to non OCaml

Emilio Jesús Gallego Arias (Mar 20 2022 at 13:02):

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

Emilio Jesús Gallego Arias (Mar 20 2022 at 13:02):

tho

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

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

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

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

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

Emilio Jesús Gallego Arias (Mar 20 2022 at 13:04):

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

Emilio Jesús Gallego Arias (Mar 20 2022 at 13:04):

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

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

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

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

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"

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

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

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

Karl Palmskog (Mar 20 2022 at 13:14):

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

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: Jun 10 2023 at 06:31 UTC