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

Prepare library for first release #195

Open
5 of 9 tasks
elisabethstenholm opened this issue May 31, 2022 · 6 comments
Open
5 of 9 tasks

Prepare library for first release #195

elisabethstenholm opened this issue May 31, 2022 · 6 comments
Labels
cleanup

Comments

@elisabethstenholm
Copy link
Collaborator

elisabethstenholm commented May 31, 2022 •
edited by fredrik-bakke
Loading

TODO
@EgbertRijke
Copy link
Collaborator

Some more suggestions for a release:

  • Write documentation
  • Write an article presenting the library

@EgbertRijke
Copy link
Collaborator

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

@elisabethstenholm
Copy link
Collaborator Author

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

@EgbertRijke
Copy link
Collaborator

EgbertRijke commented Jun 21, 2022 •
edited
Loading

Let's remove it

@jonaprieto jonaprieto mentioned this issue Feb 13, 2023
Merged
EgbertRijke pushed a commit that referenced this issue Feb 13, 2023
@jonaprieto
Nueva era (#445)
ab3ecac 
This PR improves the website in many ways. The resulting website'd be
like this one: https://jonaprieto.github.io/agda-unimath/

- Closes #440 
- Adds some progress #195 

Some new features added by this PR:

- Table of contents (navigation sidebar),
- list of contributors on Github,
- search bar,
- light and dark themes, and
- print option.

We got all this by using Mdbook. I hope this helps to prove more
theorems and people get interested in formalising more stuff using
agda-unimath.

Of course, this is a starting point, and I expect many fixes when I find
time:
Ideas that I'm sure we can get:

- Better support for latex using Katex.
- Bibtex support.
- Tikz support. 
- Copyable button for Agda snippets.
- Share options.
- Better print output.
- Hide imports at will.
@fredrik-bakke fredrik-bakke mentioned this issue Mar 12, 2023
Merged
@fredrik-bakke
Copy link
Collaborator

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.

@jonaprieto jonaprieto mentioned this issue Mar 14, 2023
Merged
@fredrik-bakke
Copy link
Collaborator

fredrik-bakke commented May 28, 2023 •
edited
Loading

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 fredrik-bakke added help wanted Extra attention is needed cleanup and removed help wanted Extra attention is needed labels Jun 4, 2023
@fredrik-bakke fredrik-bakke mentioned this issue Jun 9, 2023
Merged
@fredrik-bakke fredrik-bakke mentioned this issue Jun 21, 2023
Merged
@fredrik-bakke fredrik-bakke mentioned this issue Aug 30, 2023
Merged
fredrik-bakke added a commit that referenced this issue Oct 22, 2023
@EgbertRijke @fredrik-bakke
Refactor synthetic homotopy theory (#654)
fdc7e60 
- Hyperlinks throughout `synthetic-homotopy-theory`
- Using `coherence-square-identifications` and
`dependent-identifications` in `interval`
- Changing the order of arguments of `coherence-square-identifications`
to be the same as for maps

This PR builds on #649 and #650, and works toward progressing item 8 of
#195.

---------

Co-authored-by: Fredrik Bakke <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
cleanup
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@EgbertRijke @fredrik-bakke @elisabethstenholm