Some minor UX fixes

[robdockins]

Some minor, but important, fixes for the user experience.

[chameco]

This looks great overall. We should consider including integration tests for some of the top-level commands that lend themselves to that (goal_num stands out), and perhaps updating the manual to mention the new commands as well.

[robdockins]

I thought about testing, but its not totally clear to me what would make a good test for some of these... do you have an idea in mind for goal_num?

[robdockins]

I'm going to merge this now while everything is green. @chameco, if you have some concrete ideas for tests you'd like to see, I'm happy to add them later.

[chameco]

👍. I have some ideas for testing goal_num, but they'd be a lot nicer to write if we had a tactic for splitting conjunctions into goals. I'll include a test whenever I implement that tactic.

[robdockins]

We already have split_goal... do you have something else in mind?

For better or worse, the proof tactics we have for manipulating goals don't generate fresh numbers, those only come from the initial enumeration inside a verify command.

[chameco]

Ah, I hadn't run enable_experimental and therefore didn't spot split_goal in :env, TIL. It's unfortunate that it reuses the same goal number. I suppose we could write a test with llvm_verify on a dummy function alongside a few llvm_postconds, but that feels messy.

[robdockins]

Agreed, the whole thing is kind of a mess. It would be nice to have better ways to handle the issue of goal identification, numbering the goals as we do now is a crude solution at best.

#1195 has some ideas along these lines. I like the idea of a combinator that adds a user-configurable annotation "tag" to all the goals generated by things in it's scope.