abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

fix: locally imported lemmas not being tracked (or failure to publish when trying to link to those lemmas). #149

Closed innofarah closed 9 months ago

innofarah commented 9 months ago

The issue was rather this: when trying to damf-publish the main file, the locally imported lemma was not being found to be registered (there was a failure to publish in the first place). This is because the current damf-publish tries to link to all the lemmas used in the proof of a theorem (in the file to publish) as dependencies. Later however, I think that we might only want to link to locally skipped (unproved) or damf-imported lemmas, and possibly leave the choice of linking locally proved lemmas as damf dependencies to the user?

chaudhuri commented 9 months ago

Actually, on second thought, I think this one is also questionable. Let's discuss in the morning. I'm not entirely sure I understand the problem you're trying to solve.

innofarah commented 9 months ago

Sure, see you tomorrow