How does one declare "variables" using HTTP?

Stream: lean4

[Daniel Donnelly]

So I have this Diagram Chase Database that I'm working on, it's a Django site:
https://www.youtube.com/watch?v=V1orXCXHJS4

You should know that there is a research team https://coreact.wiki/ working on heavily commutative diagram aware application that supports Coq on the back end. For various reasons, I've decided upon Lean4. So the users will be able to draw diagrams and create proofs in the database, but I would like these proofs to usually be backed by Lean4 code.

So @Eric Wieser said we can simply connect to our Django site and grab from a diagram service the diagram data, using Lean4 HTTP / socket code itself. That is instead of trying to communicate with Lean4 in some other way, the Lean4 code itself will do the connecting.

So my next question is, how do we declare some Lean4 variables using data from the web? In particular the data is naturally already in an easy enough to understand JSON format (objects / morphisms / connectivity / label data / styling info).

[Eric Wieser]

I don't think I made a claim as strong as that. I certainly didn't say anything about HTTP.

[Daniel Donnelly]

@Eric Wieser Oh, I just filled in the gaps myself :)

[Eric Wieser]

But you can run lean with the json file as a command line argument

[Daniel Donnelly]

@Eric Wieser I have to do some format decoding first to turn it into anything

[Eric Wieser]

I don't see why you wouldn't be able to write your json to a file

[Daniel Donnelly]

@Eric Wieser It goes User drawing => (Quiver) JSON format => DB => (Quiver) JSON format => HTTP connection => Lean4 HTTP Client => Lean4 Declarations (hopefully). Or that is the mental model currently

[Daniel Donnelly]

So I get JSON (just keeping the same format) from the server, and then decode it with Lean? Or should the Django service produce Lean4 code and somehow we inject it on the client's code file?

[Daniel Donnelly]

@Eric Wieser Are you saying the server could create a .lean file from the Json? And then we import it? And the user shouldn't edit the imported, generated file?

[Eric Wieser]

I don't understand your data model here, or which parts of your system are running on your server and which are running on a users local machine

[Eric Wieser]

Are your users running lean, or are you running it within your server?

[Daniel Donnelly]

@Eric Wieser It might be both, but at least the first version will have ability for users to download the proof for example. But I would also like live editing, so that creating an arrow creates an arrow in Lean4. I don't know how to do the live editing part. So in answer to you, they will be running Lean4 (the clients), and so we want to remotely grab the definition of the arrows. Is it possible?

[Daniel Donnelly]

In other words the source the data is the database, but we interact with the database using Django code, and so the data can come in whatever form we need from a Django view (essentially an HTTP api point).

[Daniel Donnelly]

@Eric Wieser Any ideas ?

[Eric Wieser]

Is your intent that people use your tool from within an existing lean project?

[Daniel Donnelly]

Well, all proofs are going to be hosted on our site, but it's kind of part of Lean4 too, because of course we'll have proofs in there that are even already in mathlib. My hope is to promote Lean4, and also for lean4 community to use my tool as a visual diagram chaser, where possible - it won't do everything for you - it's still high code i.e.

[Daniel Donnelly]

The point is to have a browseable database of proofs in a format that can teach you how the proof works, but these proofs are for diagram / arrow theoretic questions mainly

[Daniel Donnelly]

The users will be able to for example functor a diagram completely in the database, but that operation also has an associated Lean4 proof.

[Daniel Donnelly]

So they only usually go into Lean4 when there is something that the drawing tools / database can't handle. But you could go into the Lean4 any time really.

[Daniel Donnelly]

@Eric Wieser How do i import a sibling .lean file?