Zulip Chat Archive

Stream: mathlib4

Topic: How to import a file in `test/` in another file in `test/`?


Scott Morrison (Jan 16 2023 at 02:14):

How can I import one file in test/ into another file in test/? I want to create an attribute and then use it, but can't do these in the same file.

Sebastian Ullrich (Jan 16 2023 at 09:12):

We have the same problem in core. If you want a test consisting of multiple files, you'll also need a way to tell the test framework to build these in the right order. So the best approach I'd say is to introduce a new kind of test that consists of a full Lake package (just like Lake's own tests, if you need inspiration).


Last updated: Dec 20 2023 at 11:08 UTC