Prepare library for first release

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

219 stars 70 forks source link

Prepare library for first release #195

Open elisabethstenholm opened 2 years ago

elisabethstenholm commented 2 years ago

TODO

[ ] #714
[ ] Clean up commented code
[x] Clean up unused imports (?)
[x] #479
[x] Add symbol for coproducts
[x] Syntax for Id (?)
[x] Change name of src/README (?)
[ ] Complete refactoring of synthetic homotopy theory
[ ] Make sure all files conform to guidelines

EgbertRijke commented 2 years ago

Some more suggestions for a release:

Write documentation
Write an article presenting the library

EgbertRijke commented 2 years ago

website version that corresponds statically to the release (suggested by Leo)

elisabethstenholm commented 2 years ago

Do we want to keep or remove src/labels.lagda.md?

EgbertRijke commented 2 years ago

Let's remove it

fredrik-bakke commented 1 year ago

Item 3 is resolved by #502, which adds the simplistic script scripts/remove_unused_imports.py that finds and removes unused imports. However, this script is not automatic, (it's a bit hacky and takes quite a long time to complete, e.g. 6.4 hours on my Mac for that PR) thus it will have to be occasionally rerun.

fredrik-bakke commented 1 year ago

Regarding items 1 and 2, it would be possible (and not very hard) to ban comments and holes with a pre-commit script. Additionally, we could ban --allow-unsolved-metas.

EDIT: See #715