Zulip Chat Archive

Stream: general

Topic: Almost empty top folders

Yaël Dillies (Nov 20 2021 at 18:13):

system and testing both have very little content (1 and 4 files respectively). Are people opposed to renaming system.random.basic to data.random and move everything intesting.slim_check. to tactic.slim_check.?

Scott Morrison (Nov 20 2021 at 23:44):

I would guess testing/slim_check is not under either src/tactic or test because @Simon Hudon arranged so that it was all non-meta code.

Scott Morrison (Nov 20 2021 at 23:45):

One thing to consider is what will happen to it during the port to Lean 4. If it is under src/tactic or test it won't be automatically translated. (We could still run mathport on it, but it won't be part of the automatic workflow.)

Yaël Dillies (Nov 20 2021 at 23:47):

I think either is low priority, so you tell me.

Last updated: Aug 03 2023 at 10:10 UTC