search

json-schema-org / community

A space to discuss community and organisational related things
81 stars 33 forks source link

GSoC: jsonschema.lean -- an implementation of JSON Schema in Lean #606

Open Julian opened 5 months ago

Julian commented 5 months ago

Project title

jsonschema.lean -- an implementation of JSON Schema in Lean

Brief Description

Lean is an extremely interesting and up and coming programming language created by Leo de Moura (formerly at Microsoft Research, now at Amazon) and his team. It is an "interactive theorem prover", though for our purposes what it offers is in short an ability to write a piece of software and then have the ability to formally prove properties of the software that you've written, all within the language itself ("software verification").

Let's write an implementation of JSON Schema in Lean!

Why? Here are some reasons:

Expected Outcomes

Skills Required

Mentors

@Julian

Expected Difficulty Hard

Expected Time Commitment 350 hours

PRANJALRANA11 commented 4 months ago

Hello @benjagm I would love to work on this, would you like to tell me how can i start with this

Julian commented 4 months ago

Great! A good first step is to review:

Good luck, feel free to follow up with specific questions.

PRANJALRANA11 commented 4 months ago

Sure

Sandhu-Sahil commented 4 months ago

Hi @benjagm @Julian , I have read the project requirements and am interested to work on the same, I am ready and excited to new programming language and also I have hints of functional programming, what is it and how it works not in Haskell or F# But that I am also willing to learn, it will hardly take 1-2 weeks.

would you like to tell me how can i start with this, and what are prerequisite for this

Julian commented 4 months ago

Great, have a look above!

vibhu1805 commented 4 months ago

Hi @Julian @benjagm , I am also interesed in working on this issue and willing to learn new programming language and all the above mentioned prerequisites.

doorkn-b commented 4 months ago

Hello @Julian. I'm really interested in getting involved with this project.

I have a good amount of experience with Haskell. I have been a TA for the course INF1A (INFR08025) at The University of Edinburgh tutoring Haskell and Computational Logic to around 40 students.

I also have some experience with interactive theorem provers and formal verification in Lean, Agda and Nuprl (particularly procedural proof scripts).

I was successful in being able to validate a few JSON files against it's schema. I'd love to tackle implementing a basic schema feature-- perhaps type validation for a few cases?

Any advice from your side on how I can proceed with better enabling myself for this would be much appreciated.

A little more information about the current priorities within the project would also be great.

Thanks a bunch!

Julian commented 4 months ago

Fantastic! Hi (to you and everyone).

I was successful in being able to validate a few JSON files against my schema. I'd love to tackle implementing a basic schema feature-- perhaps type validation for a few cases?

This sounds like a very good first thing to try!

Another recommendation I would have is to immediately try to write a Bowtie harness. A tutorial for doing that is here but obviously write it in Lean not Lua. You'll immediately fail every test of course, but that's a good qualification task for this issue! Write a Bowtie harness in Lean, fail every test, get 1 to pass, and yes type I think is a good easy one.

PRANJALRANA11 commented 4 months ago

Hy @Julian I have seen the tutorials and tried Bowtie with Lua and I have some questions 1 do I first need to write a JSON implementation in Lean and then integrate it with Bowtie or I am doing it wrong

Julian commented 4 months ago

That's indeed the subject of this project yep! You of course do not to do it all ahead of time.

PRANJALRANA11 commented 4 months ago

Got it but could you please explain what would I have to do right now as I am not getting clear from above

Julian commented 4 months ago

My recommendation was:

PRANJALRANA11 commented 4 months ago

got it thanks for clarifying this

BalrajDhakad commented 4 months ago

Hey, This is Balraj, And I am willing to work on this project as a part of GSOC 2024

BalrajDhakad commented 4 months ago

can you please guide me towards the 1st step that I can take in order to get involved in this project

Julian commented 4 months ago

Great! Welcome. Read through the above comments!

BalrajDhakad commented 4 months ago

okay 👍 :)

lgsurith commented 4 months ago

Hey @Julian i would love to learn more about the Lean codebase and try to contibute for the raised issue ! , any pre-requisites that i must do before moving forward with the given issue ?

Julian commented 4 months ago

Great! Glad to hear. None other than what's mentioned above!

lgsurith commented 4 months ago

Sure @Julian will start implementing right away and update you on the tasks that i complete ! Quick question are those a part of qualification task ? and also i am pretty new in the world of FOSS development so will it hinder me in any chance of getting qualified ?

Julian commented 4 months ago

Quick question are those a part of qualification task ?

For this project yes!

and also i am pretty new in the world of FOSS development so will it hinder me in any chance of getting qualified ?

Not at all, you are very welcome, and indeed the program is tailored just for people who are! (Of course that doesn't mean you're guaranteed! But you are in the right place).

lgsurith commented 4 months ago

Thank you @Julian will start implementing right away ! any repo to be forked on to be worked with ?

Julian commented 4 months ago

Not yet! Feel free to create one for your own work.

lgsurith commented 4 months ago

Alright ! Thanks @Julian .

lgsurith commented 4 months ago

also @Julian any slack channel / mailing list to be followed for further more conversation ?

PRANJALRANA11 commented 4 months ago

Hy @Julian I am facing difficulty in containerizing lean and not finding any resources also could you suggest something

Julian commented 4 months ago

also @Julian any slack channel / mailing list to be followed for further more conversation ?

There's a JSON Schema slack for our community. There's also a Lean Zulip for the Lean one.

Hy @Julian I am facing difficulty in containerizing lean and not finding any resources also could you suggest something

Hard to say without any information. The only thing I immediately know to tell you is that if you're using alpine, that's a MUSL based image, and Lean I think is less happy with MUSL than Glibc. But you should definitely be able to find some existing people containerizing Lean, I've seen it before on the Zulip certainly.

lgsurith commented 4 months ago

Hey @Julian i might have gone through Docs and implemented basics , can you guide me on the second part because i am completely lost on that part. Github Repo for Reference : https://github.com/lgsurith/JSON_SCHEMA_LEAN

Julian commented 4 months ago

I can't be more specific than that for now I'm afraid, what you have there isn't a Lean project. It might be this specific project doesn't precisely suit your skills as I'd want you to figure out how to at least get the qualification task done on your own without much help! There's no shame though if that's the case, there are other projects within the organization which may be a better fit!

lgsurith commented 4 months ago

Alright will try my best to figure it out !

ashutosh7i commented 4 months ago

Hello @Julian , i read project description, then i also read Lean documentation thoroughly, i personally am not convinced on why we should have a JSON implementation for Lean, initially i was very excited to implement, i explored and learnt Lean a bit, but then i got several questions in my mind.

we sure can implement a json lib for Lean, but who/how will someone use that for?

according to my research Lean is a "interactive theorem prover", its docs talks through language basics and tooling, we as devs use JSON for data communication over(or) network but since i say Lean mostly working on cli, How exactly someone will use our JSON lib for ?? I personally am excited to work on it, just need some clarification.

Thanks and regards, Aashutosh soni

Julian commented 4 months ago

It's slightly hard to parse your message since I think there are some typos, but I'll assume you mean "a JSON Schema implementation for Lean" rather than "JSON" in both places?

There's a brief answer to that in the issue description. Some additional answers to:

but who/how will someone use that for?

Users of Lean for one, and people interested in formally proving things about JSON Schema for another!

we as devs use JSON for data communication over(or) network but since i say Lean mostly working on cli, How exactly someone will use our JSON lib for ??

Lean is a normal programming language, so you can write programs that do whatever you'd like in it, though yes I don't know of someone using it to build what it sounds like you have in mind, namely "traditional web APIs" -- but that's just one use of JSON, it's used in many places, and very much not just for APIs over the network, even aside from Lean. It's used e.g. for serialization of datasets, to name one example. And anywhere there's a need for JSON, there's a likely need for JSON Schema.

ashutosh7i commented 4 months ago

Thanks for your reply and clarification @Julian 😄.

Sure there can be other use cases for "a JSON Schema implementation for Lean" Best of Luck🎉.

PRANJALRANA11 commented 4 months ago

Hy @Julian I have containerized the lean app and am able to take the std input from Bowtie but for returning a JSON response i was not able to find any library as i can't directly write json in lean

Julian commented 4 months ago

It's a module in Lean's standard library: https://github.com/leanprover/std4/blob/main/Std/Lean/Json.lean (and really is partially in "Lean Core") -- which shouldn't have been impossible to find :), but hopefully that helps.

benjagm commented 4 months ago

Thanks a lot for joining JSON Schema org for this edition of GSoC!!

Qualification tasks will be published as comments in the project ideas by Thursday/Friday of this week. In addition I'd like to invite you to a office hours session this thursday 18:30 UTC where we'll present the ideas and the relevant date to consider at this stage of the program.

Please use this link to join the session: 🌐 Zoom 📅 20124-02-29 18:30 UTC

See you there!

CAIMEOX commented 4 months ago

Hello @Julian I have read the requirements and comments in this issue. This project idea is very interesting and I'm glad to participate.

I'm a fan of functional languages and theorem provers, and have working with OCaml for a long time. And I have been studying theorem provers (including lean4) and type theory for the past year and I think it's time to use them to write some projects.

In the past two months I've been working with a project program that turns simple json schema into typescript type declarations so I'm familiar with basic knowlegde about json schema.

I have gone through the Docs in bowtie website and implemented basic bowtie protocol in my repo.

Thanks and regards.

Infinity-code commented 4 months ago

Hello @Julian. I am interested in this project. As a budding mathematician, I had heard about Lean when some tough theorems were validated. I would like to take this opportunity to learn Lean and contribute to this project.

adwait-godbole commented 4 months ago

Planning to tackle this one in GSoC 👍!

Julian commented 4 months ago

Cool! A reminder here just to make sure not to confuse things with the Bowtie tickets -- the qualification task on this issue is this one i.e. to start a Lean project and write a Bowtie harness in Lean which fails all the tests!

PRANJALRANA11 commented 4 months ago

Hy @Julian I had written the bowtie harness which is failing the test is this enough to pass the qualification task

Julian commented 4 months ago

Great!

Arnav-99 commented 4 months ago

Hello @Julian, I'd like to contribute to this project.

I have a year of experience in Lean 4 and am currently working on adding greater user support for co-inductive types. I'd love to channel this experience into a community-wide project!

Additionally, please correct me if I'm wrong, but this https://json-schema.org/blog/posts/bowtie-intro is the link to the JSON schema tutorial right?

Thanks!

Julian commented 4 months ago

Hi. Nice! Welcome. Thanks for your interest!

Additionally, please correct me if I'm wrong, but this https://json-schema.org/blog/posts/bowtie-intro is the link to the JSON schema tutorial right?

That's an intro post which might be worth skimming, the actual harness tutorial is here!

Arnav-99 commented 3 months ago

I'm experiencing difficulties installing Bowtie using brew on Ubuntu 20.04, any ideas why this might be occurring?

I have Python 3.12, and attached herewith is the brew output. Assistance would really help, thanks! brew_out.txt

Julian commented 3 months ago

You're the first person to try to install it via brew on Linux I suspect (and honestly the first person I've ever met who uses brew on Linux :).

It's not clear whose fault it is from that error message (whether something's broken in Linuxbrew or in Bowtie's formula).

I'd recommend installing it via pipx to get unblocked.

Arnav-99 commented 3 months ago

Alright, I will try that! Just to clarify, the pipx installation guide be carried out by substituting podman with Docker right? (It seems that the former is not compatible with versions older than Ubuntu 20.10 but the latter is)

Julian commented 3 months ago

I would expect that to be fine yeah.

benjagm commented 3 months ago

🚩 IMPORTANT INSTRUCTIONS REGARDING HOW AND WHERE TO SUBMIT YOU APPLICATION 🚩

Please join this discussion in JSON Schema slack to get the last details very important details on how to better submit your application to JSON Schema.

See communication here.

github-actions[bot] commented 1 month ago

Hello! :wave:

This issue has been automatically marked as stale due to inactivity :sleeping:

It will be closed in 180 days if no further activity occurs. To keep it active, please add a comment with more details.

There can be many reasons why a specific issue has no activity. The most probable cause is a lack of time, not a lack of interest.

Let us figure out together how to push this issue forward. Connect with us through our slack channel : https://json-schema.org/slack

Thank you for your patience :heart: