agda-unimath icon indicating copy to clipboard operation
agda-unimath copied to clipboard

Published 20 hours ago • verified publisher icon UniMath

Prepare library for first release

Open elisabethstenholm opened this issue 3 years ago • 6 comments

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

elisabethstenholm avatar May 31 '22 12:05 elisabethstenholm

Some more suggestions for a release:

  • Write documentation
  • Write an article presenting the library

EgbertRijke avatar Jun 10 '22 08:06 EgbertRijke

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

EgbertRijke avatar Jun 14 '22 11:06 EgbertRijke

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

elisabethstenholm avatar Jun 15 '22 08:06 elisabethstenholm

Let's remove it

EgbertRijke avatar Jun 21 '22 11:06 EgbertRijke

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 avatar Mar 14 '23 09:03 fredrik-bakke

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

fredrik-bakke avatar May 28 '23 07:05 fredrik-bakke