math-comp
fixing discrete topologies
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 https://github.com/math-comp/hierarchy-builder/issues/447 and https://github.com/math-comp/hierarchy-builder/issues/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
@zstone1 HB.saturate is a perfectly valid command to call. Hopefully in the future we make sure HB handles this automatically.
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?
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. https://github.com/math-comp/hierarchy-builder/pull/414
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
I've rebased, fix the changelog (but not checked it yet), and recycled documentation for the file discrete_topology but it needs to be be completed
