Dan Christensen

mailnag occasionally crashes

1

Once or twice a week, mailnag crashes and needs to be restarted. I think these are the logged messages from a crash last week. Any ideas how to debug this?...

Dependences of Nat/Core.v and DProp.v

4

We currently have some awkward, deep dependencies. For example, Nat/Core.v defines addition of natural numbers, and it depends on DProp.v, which needs Truncations/Core.v and Modalities/ReflectiveSubuniverse.v. ReflectiveSubuniverse.v needs Extensions.v, which needs...

Try to make entire library Cumulative

3

This is WIP to show what fails when you try to make the entire library Cumulative. I didn't put much effort into this. Algebra/Universal/Homomorphism.v: `homomorphism_id` fails, and I didn't immediately...

coqdoc section links don't work for alectryon and timing toc pages

1

The alectryon and timing toc pages list all of the sections within the various .v files, but when you click on one of those links, you are just taken to...

peano_naturals.v: get rid of universe N

8

This is trying to address #1722. peano_naturals.v builds fine with the changes in this PR, but the build of Classes/theory/naturals.v fails, as it can't find lots of instances. For example,...

experiment with Hint Constants Opaque in typeclass search

3

In #1779, @JasonGross suggested that typeclass search could be made faster and more predictable by having constants opaque by default and manually marked to unfold when that is appropriate. It...

global_styles.css: reduce min-height to 500px

2

With 600px, the attached window you get when clicking on the Join extension icon required a scroll bar, making the tab buttons not visible by default. 500px works for me,...

Fixes #120. If you widen the popout window, then it would refuse to open. This fixes that issue. The same ` - width` idiom is used in several other places.

As a test, I added `Types.Universe` and `Modalities.ReflectiveSubunivere` to the start of NullHomotopy.v and ran minimize-requires.py, but it didn't remove either of the unneeded imports. ``` $ git diff diff...

minimize-requires is making a .bak file for files it doesn't actually change (see file2.v below) and is making both a .bak and a .bak.bak file for files it does change...