-
-
Notifications
You must be signed in to change notification settings - Fork 34
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
GSoC: jsonschema.lean -- an implementation of JSON Schema in Lean #606
Comments
Hello @benjagm I would love to work on this, would you like to tell me how can i start with this |
Great! A good first step is to review:
Good luck, feel free to follow up with specific questions. |
This comment was marked as outdated.
This comment was marked as outdated.
Hi @benjagm @Julian , would you like to tell me how can i start with this, and what are prerequisite for this |
This comment was marked as outdated.
This comment was marked as outdated.
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! |
Fantastic! Hi (to you and everyone).
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 |
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 |
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
My recommendation was:
|
This comment was marked as outdated.
This comment was marked as outdated.
Hey, |
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
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 ? |
Great! Glad to hear. None other than what's mentioned above! |
Sure @Julian will start implementing right away and update you on the tasks that i complete ! |
For this project yes!
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). |
Thank you @Julian will start implementing right away ! any repo to be forked on to be worked with ? |
Not yet! Feel free to create one for your own work. |
Alright ! Thanks @Julian . |
also @Julian any slack channel / mailing list to be followed for further more conversation ? |
Hy @Julian I am facing difficulty in containerizing lean and not finding any resources also could you suggest something |
There's a JSON Schema slack for our community. There's also a Lean Zulip for the Lean one.
Hard to say without any information. The only thing I immediately know to tell you is that if you're using |
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. |
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! |
Alright will try my best to figure it out ! |
Hello @Julian , we sure can implement a json lib for Lean, according to my research Lean is a "interactive theorem prover", its docs talks through language basics and tooling, Thanks and regards, |
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:
Users of Lean for one, and people interested in formally proving things about JSON Schema for another!
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. |
Thanks for your reply and clarification @Julian 😄. Sure there can be other use cases for "a JSON Schema implementation for Lean" |
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 |
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. |
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: See you there! |
Hello @Julian 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. |
Hello @Julian. I am interested in this project. |
Planning to tackle this one in GSoC 👍! |
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! |
Hy @Julian I had written the bowtie harness which is failing the test is this enough to pass the qualification task |
Great! |
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! |
Hi. Nice! Welcome. Thanks for your interest!
That's an intro post which might be worth skimming, the actual harness tutorial is here! |
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! |
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. |
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) |
I would expect that to be fine yeah. |
🚩 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. |
Hello! 👋 This issue has been automatically marked as stale due to inactivity 😴 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 ❤️ |
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
The text was updated successfully, but these errors were encountered: