metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
26 stars 11 forks source link

Incremental builds #38

Open tirix opened 2 years ago

tirix commented 2 years ago

This means reloading a database, and providing an updated version for all passes.

Ideally we would like to provide functions which a server could use to support to LSP protocol, even though such a server would be outside of the scope of this library.

Interestingly, LSP provides document synchronization with a notification each time a document changes. This could allow incremental passes over the database, where e.g only the segment which have changed would be rebuilt.

However this also requires to be well thought within the library (e.g. Atom numbering would change with an incremental build). SMM provided some functionality and/or provision for this.