search

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

Improve CI pipeline #11

Closed tirix closed 2 years ago

tirix commented 3 years ago

Add pre-push requirements or CI requirements, enforcing formatting and clippy fixes, and running whatever tests are available, including against the latest version of set.mm and iset.mm.

I propose adding the following items to the CI:

david-a-wheeler commented 3 years ago

We already have a CI pipeline, it's implemented in metamath-knife/.github/workflows/verify.yml.

You just want to improve the CI pipeline to test more things. Which is fine! But I think you just need to tweak what's there.

tirix commented 3 years ago

Yes! I'll be adding more tests. There are already a few new simple ones in commit f6947c1.

Also, what I'd like to do with cargo clippy is described here. We could probably do the same with cargo fmt.

tirix commented 2 years ago

(Updated the initial comment with a to-do list)

tirix commented 2 years ago

With #26 , I've included a test against an official set.mm, albeit always the same version. I'm not sure whether we shall periodically update that version, other rather actually check against the latest version.

digama0 commented 2 years ago

I think it should run against latest master. This introduces some nondeterminism into CI, since upstream changes could cause a mm-knife PR to break, but it seems like an easy way to periodically check things without burning too much CI resources. Every set.mm master commit should be reliable anyway because of its own CI.

tirix commented 2 years ago

I agree that would be a good middle ground.

The latest master corresponds to August 2020 and does not have the 'parser hints' we unfortunately still need. I shall ask Norm to merge it. Maybe it's the right time to do so, just before we change the definition of non-free!

tirix commented 2 years ago

All proposed improvements are included, I'm closing this issue. We may still add iset.mm later on.