Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

The CI doesn't check for duplicate titles in pull requests #552

Closed
EgbertRijke opened this issue Apr 8, 2023 · 1 comment · Fixed by #579
Closed

The CI doesn't check for duplicate titles in pull requests #552

EgbertRijke opened this issue Apr 8, 2023 · 1 comment · Fixed by #579
Assignees
@jonaprieto

Comments

@EgbertRijke
Copy link
Collaborator

We are getting the following error:

WARNING! Duplicate titles in elementary-number-theory:
[1165](https://github.com/UniMath/agda-unimath/actions/runs/4643712723/jobs/8218501662#step:12:1166)
  Title 'Inequality on integer fractions': inequality-integer-fractions, inequality-rational-numbers
[1166](https://github.com/UniMath/agda-unimath/actions/runs/4643712723/jobs/8218501662#step:12:1167)
  Title 'The rational numbers': rational-numbers, reduced-integer-fractions
[1167](https://github.com/UniMath/agda-unimath/actions/runs/4643712723/jobs/8218501662#step:12:1168)
make: *** [SUMMARY.md] Error 2

Ideally, the CI would catch this when it checks a PR, but currently it doesn't catch these kinds of errors.
@EgbertRijke EgbertRijke changed the title Github actions doesn't check for duplicate titles in pull requests The CI doesn't check for duplicate titles in pull requests Apr 8, 2023
@jonaprieto
Copy link
Collaborator

I would expect this issue to be solved by #564, but I'm not sure until I see it running. Perhaps, you can try it now and see if we catch the error with the new setup.

@fredrik-bakke fredrik-bakke mentioned this issue Apr 27, 2023
Merged
EgbertRijke pushed a commit that referenced this issue Apr 28, 2023
@fredrik-bakke
Miscellaneous refactoring and small additions (#579)
e2100fb 
### Highlights
- Rename the binary operator for the wedge of pointed types from `_∨_`
to `_∨*_`.
- Add binary operator notation for the following
  - propositional disjunction `_∨_`
  - propositional conjunction `_∧_`
  - pointed homotopy `_~*_`
  - pointed function composition `_∘*_`
  - addition on natural numbers `_+ℕ_`
- Define pointed cartesian product `_×*_` and pointed dependent sum `Σ*`
  (we could similarly add the notation `Π*`)
- Cleanup of sign homomorphism delooping files (I don't know what's
wrong with me, but please see questions below)
- Rename `cone-pullbacks` to `cones-over-cospans`, and `cocone-pushouts`
to `cocones-under-spans`, as this more closely represents what the files
contain
- Define pullback cones
- Define preidempotent maps
- Eradicate use of `i j k` for universe levels
- Disambiguate Precat definitions from type definitions
- Add `pre-commit` check for issue discussed in #573 
- Add `generate-main-index-file` to `pre-commit`, resolves #552 
- Print errors to `sys.stderr`. #532 may be fixed by this
- Better `pre-commit` hook ordering
- Fix a couple of mistakes in the Makefile
- Remove unused imports
- Fully capitalize the name of the universe of decidable propositions
`Decidable-Prop`
- Add `imports` task that minimizes module imports, and add details to
all the tasks.

Sorry for the mess!
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jonaprieto jonaprieto

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Miscellaneous refactoring and small additions fredrik-bakke/agda-unimath
2 participants
@EgbertRijke @jonaprieto