Auto-generate exercise files

This implements a make exercises target which auto-generates the exercise files from the solutions. I hope the syntax is self-explaining:

(* BEGIN SOLUTION *)
  solution here.
(* END SOLUTION *)

is replaced by

  (* exercise *)
Admitted.

and the more powerful

(* BEGIN SOLUTION *)
  solution here.
(* END SOLUTION BEGIN TEMPLATE
  exercise template here.
END TEMPLATE *)

is replaced by

  exercise template here.

Fixes #4 (closed)

@robbertkrebbers please let me know what you think :)

Seems good to me! Thanks a lot.

It would be good to document the syntax in README.md (basically, just copy the MR description into that file).

added 1 commit

• 5bc2d52c - expand README

Compare with previous version

@robbertkrebbers I extended the README with the MR description.

LGTM!

What we currently do not have is CI to ensure that the exercise files do not get out of sync... how important to you think that is?

I think it would be nice if the CI were to check this.

Don't we have the same for the test ref files? (Well, there the test will typically fail...)

For test files, make checks the ref tests.

We don't want that here, as we want people to edit the exercises and make them. So we'd need to add a make check target or so and make CI run that. And I'd need to code the logic for doing the check...^^

I suppose we could put that on the "wish list". This MR is a strict improvement over the current situation after all.

If we can rely on this running in a git checkout (i.e., if we make this CI-only), it actually shouldn't be too hard. We just run the target and fail if git notices any changes. Then we don't need to do the diffing ourselves.

I'll try that.

added 1 commit

• a6c95521 - forgot to add Makefile.coq.local

Compare with previous version

Okay I think that should do it, at least locally it works fine. :) I'll est on a CI branch as well but let's merge this one in the mean time.

mentioned in commit fcc95c24

merged

Great!

mentioned in merge request tutorial-popl20!2 (merged)