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

Markdown conventions script does not trigger on ill-formed code blocks #704

Closed
fredrik-bakke opened this issue Aug 22, 2023 · 0 comments · Fixed by #705
Closed

Markdown conventions script does not trigger on ill-formed code blocks #704

fredrik-bakke opened this issue Aug 22, 2023 · 0 comments · Fixed by #705
Assignees
@fredrik-bakke
Labels
bug Something isn't working pre-commit

Comments

@fredrik-bakke
Copy link
Collaborator 

          Wait, but then "Markdown conventions", which checks for well-formatted code blocks, should have triggered, right? Which it didn't?

Originally posted by @VojtechStep in #703 (comment)
@fredrik-bakke fredrik-bakke added bug Something isn't working pre-commit labels Aug 22, 2023
@fredrik-bakke fredrik-bakke self-assigned this Aug 22, 2023
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this issue Aug 22, 2023
@fredrik-bakke
Fix UniMath#704
7a45f75
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this issue Aug 22, 2023
@fredrik-bakke
Squashed commit of the following:
e36ae09 
commit b02a0ad
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 22 13:19:51 2023 +0200

    file-conventions simplification

commit 7a45f75
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 22 13:13:14 2023 +0200

    Fix UniMath#704

commit a37f4f2
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 22 11:42:54 2023 +0200

    vscode ignore pull requests in `master`

commit 2c189a0
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 22 11:42:32 2023 +0200

    Fix `os.walk` yields directories that don't exist
    Probably due to caching

commit 165321c
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 21 23:08:26 2023 +0200

    Cyclic groups (UniMath#697)

    This PR introduces cyclic groups to the library, in several equivalent
    forms.

    ---------

    Co-authored-by: Fredrik Bakke <[email protected]>

commit 85d19a5
Author: maybemabeline <[email protected]>
Date:   Mon Aug 21 21:24:18 2023 +0200

    Refactor nilradical proof for prime ideals (UniMath#699)

    I refactored the proof that the nilradical is included in every prime
    ideal as discussed in the discord server. I also added some auxiliary
    functions for prime ideals viewed as radical ideals. Regarding the last
    function, I wasn't sure whether to keep it because agda accepts
    membership in a prime ideal and in the corresponding radical ideal as
    definitionally equal, but in the nilradical proof it feels wrong to
    prove something for prime ideals using a function about radical ideals
    directly.
    I also wasn't sure whether the naming of these functions follows
    conventions correctly.

    ---------

    Co-authored-by: Fredrik Bakke <[email protected]>

commit 34c2ecf
Author: Raymond Baker <[email protected]>
Date:   Sun Aug 20 04:16:03 2023 -0600

    Dependent Universal Property of Suspensions (UniMath#690)

    This pr contains:

    - the definition of a dependent suspension structure
    - the definition of the function dependent-ev-suspension
    - the definition of the dependent universal property of suspensions

    ---------

    Co-authored-by: Egbert Rijke <[email protected]>
    Co-authored-by: Fredrik Bakke <[email protected]>

commit 7c87d5f
Author: Fredrik Bakke <[email protected]>
Date:   Fri Aug 18 16:26:57 2023 +0200

    Compatibility patch agda-mode (UniMath#698)

    A compatibility patch for version `0.4.0` of agda-mode. With this
    version, agda-mode defined its own file format for literate agda
    markdown files, conflicting with the file format defined by agda-syntax.

commit 7ef1685
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 14 11:04:53 2023 +0200

    adding overview to installation guide (UniMath#695)

commit 12e37b1
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 7 15:53:53 2023 +0200

    Recovering the guidelines for direct clones (UniMath#694)

commit 7fc8097
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 7 14:23:29 2023 +0200

    Normalizers, normal closures, normal cores, and centralizers (UniMath#693)

    This PR adds normalizers, normal closures, normal cores, and
    centralizers to the library.

commit 58ce51d
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 7 10:34:46 2023 +0200

    Guidelines for forking the repository and creating branches within clone (UniMath#692)

commit 7608668
Author: Egbert Rijke <[email protected]>
Date:   Mon Aug 7 09:17:33 2023 +0200

    Recommend cloning shallow library (UniMath#691)

    This PR recommends users to clone a shallow copy of the library, to
    address UniMath#689.

commit 37c577e
Author: Raymond Baker <[email protected]>
Date:   Mon Aug 7 00:21:29 2023 -0600

    suspension loop space adjunction (UniMath#688)

    This pr contains:
    - definition of the underlying map of the equivalance
    - definition of the underlying map of the inverse

    Proof that these maps are in fact inverses of each other must wait until
    another pr since I first must formalize the dependent universal property
    of suspensions

commit 013e3f5
Author: Egbert Rijke <[email protected]>
Date:   Thu Aug 3 11:48:37 2023 +0200

    Adding comments to the style guides that (subsection) titles should be on one line (UniMath#687)

    ...even if they are longer than the 80 character line limit.

commit dd04229
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 1 14:33:32 2023 +0200

    Small constructions from large ones in order theory (UniMath#680)

    Defines
    - small semigroups from large semigroups
    - small preorders from large preorders
    - small posets from large posets
    - small suplattices from large suplattices
    - small meet semilattices from large meet semilattices
    - large preorders are large precategories
    - large posets are large categories

commit 3dce59f
Author: Fredrik Bakke <[email protected]>
Date:   Tue Aug 8 13:40:43 2023 +0200

    small edits

commit 4f8e685
Author: Fredrik Bakke <[email protected]>
Date:   Sat Aug 5 23:02:04 2023 +0200

    redefine wide function classes to contain all equivalences

commit f60a810
Author: Fredrik Bakke <[email protected]>
Date:   Sat Aug 5 22:53:32 2023 +0200

    Having equivs is the same as having identities

commit 126c487
Author: Fredrik Bakke <[email protected]>
Date:   Sat Aug 5 21:18:34 2023 +0200

    random fixes
@fredrik-bakke fredrik-bakke mentioned this issue Aug 22, 2023
Merged
EgbertRijke pushed a commit that referenced this issue Aug 23, 2023
@fredrik-bakke
Pre-commit fixes and some miscellaneous changes (#705)
4d09c2e 
Resolves #704 and fixes some other previously unidentified bugs with the
pre-commit hooks. Specifically, `os.walk` sometimes return non-existent
directories (likely due to caching), and the
`generate_namespace_index_module` hook didn't autogenerate titles like
it was supposed to.

Also, do some miscellaneous refactoring that I had lying around. Of
note, I change the definition of orthogonal factorization systems to
contain all equivalences instead of just identity maps, although these
conditions are equivalent assuming univalence.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@fredrik-bakke fredrik-bakke

Labels
bug Something isn't working pre-commit
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Pre-commit fixes and some miscellaneous changes fredrik-bakke/agda-unimath
1 participant
@fredrik-bakke