Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add info about verification status #16

Open
SReichelt opened this issue Jan 27, 2019 · 0 comments
Open

Add info about verification status #16

SReichelt opened this issue Jan 27, 2019 · 0 comments
Assignees
Labels
component: gui Issue concerns the web-based user interface component: hlm logic Issue concerns the HLM logic enhancement New feature or request good first issue Good for newcomers

Comments

@SReichelt
Copy link
Owner

SReichelt commented Jan 27, 2019

Add overlay icons to library items to distinguish

  • fully proved theorems (green),
  • theorems that lack a proof (yellow),
  • theorems that have one or more proofs but none of them are fully verified from first principles (no icon, but the user should be able to find out where the gaps are),
  • definitions or theorem statements where inline or well-definedness proofs are missing (yellow, but at some point we will no longer accept such submissions),
  • definitions or theorem statements where inline proofs depend on unproved results (also yellow?), and
  • definitions where everything is OK (no icon).

When submitting a proof, at least the icon of that item should be updated immediately. In general, the verification status could be determined during a check of the entire library, see #18. It should probably be stored in the _index.slate files; if the library check touches those, that's OK.

Possibly include more info about dependencies, like e.g. in Metamath.

@SReichelt SReichelt added enhancement New feature or request component: hlm logic Issue concerns the HLM logic component: gui Issue concerns the web-based user interface labels Jan 27, 2019
@SReichelt SReichelt added this to the 2. Web-based proof input milestone Jan 27, 2019
@SReichelt SReichelt self-assigned this Jan 27, 2019
@SReichelt SReichelt added the good first issue Good for newcomers label Jan 6, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
component: gui Issue concerns the web-based user interface component: hlm logic Issue concerns the HLM logic enhancement New feature or request good first issue Good for newcomers
Projects
None yet
Development

No branches or pull requests

1 participant