Documentation and License

[YJDoc2]

Hey, This is a really amazing project!

I was going through the paper and the examples, and I feel that providing a documentation for the components along with examples can be really helpful for someone new to this. I checked through the source files, the readme and other repos and branches, and couldn't find any documentation.

In case you would be fine with it, I'd like to help in documenting the components and their examples.

Also If this is a framework which you would be making available for others to use, can you add an open-source license to this?

Thanks :)

[willcrichton]

Thanks @YJDoc2. I'll add a license later today.

For documentation, hold off on that for a bit. Right now it's open-source just to show the proof-of-concept. I intend to clean up the repo a bit before it's ready for other people to write their papers with it. For example, the build process is a bit ad hoc.

[YJDoc2]

Hey, thanks for the reply 👍

Sure, I'll keep checking occasionally for the documentation start. Also if you need help with anything, let me know, I'd like to try and help as much as I can 😄

Another thing, I might have found a bug / feature (?) :

on https://willcrichton.net/nota/ , in Modular Program Slicing through Ownership paper, section 3.1 Syntax,
In the figure 1, if we click on &r1 , it opens up the definition as expected, but then in the first definition, for the
Expression E ::= ...| pi := e | ... I believe the definition is recursive, so when you click on the pi := e it opens the same definition again, and again and again, shifting each upward , which can eventually end up as:

The tool tip started on &r1 symbol, in the big letprov<> equation below, which is not seen in the picture.

If it is a feature, cool 😅 , otherwise, if the clicked thing expands to same definition, then probably it should not create a new definition above (?). I don't particularly understand things mentioned in the paper, so I might be wrong.

Other than this, feel free to close this issue.
Thanks :)