search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
13 stars 5 forks source link

Notes make the results non-JSON #140

Closed david-a-wheeler closed 1 year ago

david-a-wheeler commented 1 year ago

If you "export to JSON" and add any "notes", the result is typically NOT a JSON file, and it's certainly not a JSON file with a single root object.

I propose adding a new field "notes" to the top-level JSON object, and store notes there. Otherwise it's not a JSON format result, creating problems for other tools.

expln commented 1 year ago

The purpose of the notes and the timestamp is to be outside the JSON when you collect few JSON states in a single file in the form of a log. For example, after saving a few states with the timestamp and notes you may end up having something similar to this:

my-proof-log.txt:

2023-07-16T21:17:18.922Z note {"srcs":[{"typ":"Local","fileName":"set.mm",...
2023-07-16T21:17:40.622Z another note {"srcs":[{"typ":"Local","fileName":"...
2023-07-16T21:17:57.428Z yet another note {"srcs":[{"typ":"Local","fileNam...

If you need a pure JSON with some description inside, you should not add the timestamp and notes, but instead add the description to the description field in the editor before exporting.

expln commented 1 year ago

Looks like there is nothing to change. I am closing this issue. Please feel free to re-open it if anything in this issue remained without answer.