fixing discrete topologies

[zstone1]

Adding discrete topologies, uniformities, and metrics to the hierarchy. Cleans up a bunch of pre-HB issues, and now we can use bool directly instead of through a bunch of aliases. We can now just write cantor_space = prod_topology (fun=> bool) and Uniform.on cantor_space. Pretty nice!

However, I encountered a lot of weird HB errors. I put in tickets math-comp/hierarchy-builder#447 and math-comp/hierarchy-builder#446

Furthermore, I could only get this to compile with a call to HB.saturate. This is fine, except that it the commands takes several minutes to run. And is broken on master with error

Error: The elpi tactic/command HB.saturate failed without giving a specific
error message. Please report this inconvenience to the authors of the
program.

I am skeptical if I get a build that works on both master and the current release

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[CohenCyril]

@zstone1 HB.saturate is a perfectly valid command to call. Hopefully in the future we make sure HB handles this automatically.

[zstone1]

The problem I'm having is that it takes 3 minutes to run that one command. Since I know what structure i want it to saturate for, is there anyway for me to improve its performance?

[CohenCyril]

The problem I'm having is that it takes 3 minutes to run that one command. Since I know what structure i want it to saturate for, is there anyway for me to improve its performance?

Yes, but in the next HB release. math-comp/hierarchy-builder#414

[zstone1]

All the reshuffling of topology_theory seems to have unblocked this. Although the underlying issue is probably still around, this is now ready for a proper review