coq / coq-bench

Scripts for differential performance testing of Coq packages / versions
Other
4 stars 6 forks source link

Make coq-bench per-line timing script work with coq-lambda-rust #80

Closed JasonGross closed 4 years ago

JasonGross commented 4 years ago

When you opam install coq-lambda-rust, you get something like coq-lambda-rust.dev.2020-03-21.0.73f3ded1, not coq-lambda-rust.dev. This is a conservative change that supports such timestamping. This will go wrong if any packages ever decide to name their dev versions something other than package-name.dev followed by something. We could be more permissive and allow $coq_opam_package*, but then if two packages share the same prefix, things will go wrong. It would be nice if we could get opam to give us the name of the folder, but this should work for the foreseeable future.

Note that the wildcard gets expanded on the calls to cd and timelog2html. Things will go wrong if there are multiple folders matching the pattern (cd will fail with -bash: cd: too many arguments; find will look for all the .vo files in the current directory (not sure what that will be at this point), and timelog2html will get too many arguments (not sure what it will do with them)). I think this is okay, though, since we don't expect there to be multiple matches, unless the naming scheme changes drastically (or, I suppose, if we end up with both coq-A and coq-A.dev as separate opam packages, giving us the folders coq-A.dev and coq-A.dev.dev; hopefully no-one does this.)

cc @ppedrot