mathport icon indicating copy to clipboard operation
mathport copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Port tests

Open gebner opened this issue 3 years ago • 3 comments

It would be nice if CI could also synport the test and archive directories of mathlib. Particularly the tests would be super helpful to get test cases for ported tactics without much effort.

gebner avatar Nov 30 '21 14:11 gebner

@gebner, this isn't immediately trivial. mathport gives an error when it meets relative imports, and in mathlib it seems essential to use relative imports in test (and in archive).

kim-em avatar Dec 01 '21 08:12 kim-em

There are six relative imports in total, I think it would be completely okay to just ignore them (for now).

gebner avatar Dec 01 '21 09:12 gebner

There are six relative imports in total, I think it would be completely okay to just ignore them (for now).

Okay, trying it out in #64.

kim-em avatar Dec 02 '21 03:12 kim-em