dwrensha / compfiles Goto Github PK

Hello. The command in this repository to extract answers from a problem is nice. I've been thinking of making a collection of questions in Lean too, but...

• Including the answers in the source would immediately spoil it.
• If I don't include the answers in the source, I can't automatically check whether the problem is correct or not.

I was troubled by this dilemma. Your command solves my problem.

Can you release just the extractProblems command as a separate package? I don't want to import the whole compfiles just to use the extractProblems command.

Thank you.

It's a bad experience if users see a CI error that tells them to run mk_toplelevel_file.bash, but then running it just makes things worse.

Currently on MacOS, the script inserts an extra dot in each import name.

I think it's an interesting project.

Want to make your web site look more stylish? I suggest using SSGs such as Zola or mdbook.