Window.localStorage for persistence

[vassilmladenov]

Hi, I found this project from this thread and I love it, thank you for building this! This is so much easier and more portable than installing opam and Coq if you just want to do a few examples. Would you be willing to add support for something like Chrome's local storage to save filled-out proofs and keep track of progress?

[corwin-of-amber]

Hi, thanks! This is definitely in our to-do list. In fact, localStorage is utilized in jsCoq's scratchpad, which is a single-file editor, and we've discussed with @bcpierce00 some options on how to integrate it into literate pages. What's stopping us now is mainly the fact that the SF books are constantly evolving, by design, and this potentially causes some impedance between what the learner types in and changes made to the book itself. A git-style conflict resolution scheme would be quite an undertaking and might be an overkill in this context. We are considering some lightweight solutions. Would love to hear your ideas!

[vassilmladenov]

A git-style conflict resolution scheme would be quite an undertaking and might be an overkill in this context. We are considering some lightweight solutions. Would love to hear your ideas!

Honestly, I wasn't even thinking about conflict resolution. I'd be more fine if it was just indexed by the hash of the file and if the content changes I lose my saved stuff / I have to manually recover it from localStorage. Just wanted to be able to refresh to reset Coq's state if something screws up!

[ejgallego]

@vassilmladenov , a possible way to go forward is to add an IRMIN backend where users can save the (textual) pages.

Users could configure were to place IRMIN's data (either a git repos, or local storage)

[vassilmladenov]

@ejgallego I haven’t heard of this package before! Looks neat, lots of reading to do