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

Swap from md to text code blocks #622

Merged
merged 4 commits into from
May 16, 2023
Merged

Swap from md to text code blocks #622

merged 4 commits into from
May 16, 2023

Conversation

fredrik-bakke
Copy link
Collaborator

  • Fix diagrams in pullback-hom
  • Swap from md to text code blocks
  • Register Collatz' bijection in the OEIS file

@EgbertRijke
Copy link
Collaborator

Cool! Did you compile the website locally to see whether it looks good?

@fredrik-bakke
Copy link
Collaborator Author

oh, uh, no. I don't know how to do that 😅

@fredrik-bakke
Copy link
Collaborator Author

But I also have to run, so can't do it now

@EgbertRijke
Copy link
Collaborator

No worries. I'm also travelling at the moment. The command for compiling the website is make website

@fredrik-bakke
Copy link
Collaborator Author

fredrik-bakke commented May 14, 2023 •
edited
Loading

I'm getting these errors when I try to make website:

2023-05-14 21:11:25 [WARN] (mdbook::preprocess::cmd): The command wasn't found, is the "catppuccin" preprocessor installed?
2023-05-14 21:11:25 [WARN] (mdbook::preprocess::cmd):   Command: mdbook-catppuccin
2023-05-14 21:11:25 [ERROR] (mdbook::utils): Error: Unable to start the "katex" preprocessor. Is it installed?
2023-05-14 21:11:25 [ERROR] (mdbook::utils):    Caused By: No such file or directory (os error 2)
make: *** [website] Error 101

I've tried installing katex and @catpuccin/palette through npm, but this changed nothing. What do I need to do?
As an aside, I think our installation guide should include steps for how to set up one's system for building the website.
Also, I'm wondering, how do I view the web pages once it's built? Do I need to host it locally somehow?

@VojtechStep
Copy link
Collaborator

There's a make target to install the website dependencies, assuming you have Rust installed (it uses cargo): make install-website-dev. Then to build the website you run make website, and to open it you run make serve-website (it takes a second to start the web server, and IIRC then it should open up the page in your browser automatically).

This should probably be documented somewhere.

@fredrik-bakke
Copy link
Collaborator Author

image

Looks good to me! 😄 Thanks for the help, Vojtech!

@EgbertRijke EgbertRijke merged commit f19a7c9 into UniMath:master May 16, 2023
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request May 18, 2023
@fredrik-bakke
Swap from md to text code blocks (UniMath#622)
e3f8a25 
- Fix diagrams in `pullback-hom`
- Swap from `md` to `text` code blocks
- Register Collatz' bijection in the OEIS file
@fredrik-bakke fredrik-bakke deleted the fix2 branch May 21, 2023 21:28
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request May 28, 2023
@fredrik-bakke
Squashed commit of the following:
f64c83c 
commit 3b74252
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 27 22:51:21 2023 -0400

    fix indentation

commit 880504d
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 27 21:03:31 2023 -0400

    remove punctuation at end of headers

commit cb2a09c
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 27 21:03:15 2023 -0400

    pre-commit autoremove punctuation at end of header

commit f19934c
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 27 20:52:42 2023 -0400

    add remarks about missing contents

commit 582e75c
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 27 20:34:57 2023 -0400

    pre-commit detect empty sections at end of file

commit 3d53688
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 27 19:45:19 2023 -0400

    remove empty code blocks

commit 437056c
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 27 19:45:04 2023 -0400

    compatibility markdown-conventions and fix-imports

commit 8c7f782
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 27 19:38:57 2023 -0400

    pre-commit autoremove empty code blocks

commit 6f84849
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 14:28:44 2023 +0200

    fix some indentation and then give up for the moment

commit ccdad61
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 14:05:31 2023 +0200

    add `indentation_conventions.py`

commit ba930b4
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 13:33:11 2023 +0200

    rename pre-commit scripts

commit 2cd2433
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 13:09:02 2023 +0200

    Add and enforce section conventions

commit db60c6f
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 12:07:41 2023 +0200

    rename `remove_extra_blank_lines.py`
    to `blank_line_conventions.py`

commit 0d1f085
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 12:05:11 2023 +0200

    Fix top section headers not at start of file

commit 986a68d
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 11:52:20 2023 +0200

    swap to using `_-ℤ_`

commit cea0cf6
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 10:53:52 2023 +0200

    define infix operator `_-ℤ_` for difference

commit b2cd359
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 10:44:42 2023 +0200

    Fix empty subsubsections

commit ecd6061
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 10:05:23 2023 +0200

    fix empty subsections

commit 3823a10
Merge: 23e5534 92c52ba
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sun May 21 06:43:30 2023 +0200

    Merge branch 'UniMath:master' into modalities3

commit 23e5534
Author: Jonathan Cubides <jonathan.cubides@uib.no>
Date:   Fri May 19 01:04:26 2023 +0200

    Fix: missing logo (UniMath#625)

    Minor fix due to a local cache issue

commit 0ba07cd
Author: Jonathan Cubides <jonathan.cubides@uib.no>
Date:   Fri May 19 00:09:46 2023 +0200

    Enable  TOC  and fix minor warnings (UniMath#602)

    - Enhance TOC
    - Solves some warnings seen here:
    https://github.com/UniMath/agda-unimath/actions/runs/4991616992/jobs/8939272325#step:12:1304
    - Closes UniMath#614
    - Removes the background from the agda logo.

    I tried syncing SVG stroke colours with agda-logo.css (so it responds to
    the colour theme), but no luck yet. We need more time to figure it out.
    the following is related and the suggestion included in my experiment.

    - rust-lang/mdBook#773

    ---------

    Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>

commit 9b80ef0
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 13 20:29:54 2023 +0200

    Remove unused imports and fix some unaddressed comments (UniMath#621)

    Sorry, my script wasn't finished when I made the last commit in UniMath#620,
    and here are the remaining unused imports. This PR also fixes some
    comments I made earlier that went unaddressed.

    I'm wondering, are the imports scripts interfering with people's merging
    process a lot? If so, we don't have to merge those changes now.

commit 3b658d0
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 13 19:14:02 2023 +0200

    Refactor to use infix binary operators for arithmetic (UniMath#620)

    - Refactor to use infix binary operators for arithmetic.
    - Define infix binary operators for arithmetic operations on the
    Eisenstein integers, Gaussian integers,half integers, and truncation
    levels.
    - Swap to using left/right instead of a `'` for different laws for
    binary arithmetic operators.
    - Some additional refactoring for Eisenstein integers and Gaussian
    integers

    Note that the non-infix variants of the operators are still used some
    places, matching how `Id` and `pair` are used.

commit f77b71e
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 13 14:39:13 2023 +0200

    Define binary operator notations for `mul-ℕ`, `mul-ℤ`, and `exp-ℕ`. (UniMath#618)

    They are `_*ℕ_`, `_*ℤ_`, and `_^ℕ_` respectively.

    In addition to what the title says, I've also refactored the files
    - `multiplication-natural-numbers`
    - `multiplication-integers`
    - `exponentiation-natural-numbers`
    - `absolute-value-integers`

    to use the binary operators where it's natural, to get a sense for how
    this would look. It should be possible to change most usages easily
    enough* with a nice enough regex, but I don't want to do this before I
    get some feedback on whether it is preferable.

    Also, pairs like `is-injective-mul-succ-ℕ` and
    `is-injective-mul-succ-ℕ'` should perhaps be renamed to something like
    `is-injective-left-mul-succ-ℕ` and `is-injective-right-mul-succ-ℕ`.

commit ee5a96c
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri May 12 00:52:35 2023 +0200

    Subframes and quotient locales via nuclei (UniMath#613)

commit 750f151
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 20 17:16:03 2023 +0200

    small fixes

commit e1f3af4
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 20 00:40:58 2023 +0200

    add `is-emb-map-prod`

commit 973a00f
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 20 00:40:29 2023 +0200

    fix expressions in some headers

commit e3f8a25
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue May 16 14:05:02 2023 +0200

    Swap from `md` to `text` code blocks (UniMath#622)

    - Fix diagrams in `pullback-hom`
    - Swap from `md` to `text` code blocks
    - Register Collatz' bijection in the OEIS file

commit c7398a7
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 13 20:29:54 2023 +0200

    Remove unused imports and fix some unaddressed comments (UniMath#621)

    Sorry, my script wasn't finished when I made the last commit in UniMath#620,
    and here are the remaining unused imports. This PR also fixes some
    comments I made earlier that went unaddressed.

    I'm wondering, are the imports scripts interfering with people's merging
    process a lot? If so, we don't have to merge those changes now.

commit 001e8d7
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 13 19:14:02 2023 +0200

    Refactor to use infix binary operators for arithmetic (UniMath#620)

    - Refactor to use infix binary operators for arithmetic.
    - Define infix binary operators for arithmetic operations on the
    Eisenstein integers, Gaussian integers,half integers, and truncation
    levels.
    - Swap to using left/right instead of a `'` for different laws for
    binary arithmetic operators.
    - Some additional refactoring for Eisenstein integers and Gaussian
    integers

    Note that the non-infix variants of the operators are still used some
    places, matching how `Id` and `pair` are used.

commit fde878d
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Sat May 13 14:39:13 2023 +0200

    Define binary operator notations for `mul-ℕ`, `mul-ℤ`, and `exp-ℕ`. (UniMath#618)

    They are `_*ℕ_`, `_*ℤ_`, and `_^ℕ_` respectively.

    In addition to what the title says, I've also refactored the files
    - `multiplication-natural-numbers`
    - `multiplication-integers`
    - `exponentiation-natural-numbers`
    - `absolute-value-integers`

    to use the binary operators where it's natural, to get a sense for how
    this would look. It should be possible to change most usages easily
    enough* with a nice enough regex, but I don't want to do this before I
    get some feedback on whether it is preferable.

    Also, pairs like `is-injective-mul-succ-ℕ` and
    `is-injective-mul-succ-ℕ'` should perhaps be renamed to something like
    `is-injective-left-mul-succ-ℕ` and `is-injective-right-mul-succ-ℕ`.

commit 76bf8c7
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri May 12 00:52:35 2023 +0200

    Subframes and quotient locales via nuclei (UniMath#613)

commit 375210c
Author: VictorBlanchi <76261859+VictorBlanchi@users.noreply.github.com>
Date:   Thu May 11 16:49:27 2023 +0200

    Iterated cartesian product is closed by permutation (UniMath#617)

    I have shown that the 3 definitions of iterated cartesian product of
    types is closed by permutation.

commit 730861a
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu May 11 15:51:39 2023 +0200

    alignment of pullback-hom diagrams

commit dab6d30
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu May 11 12:33:08 2023 +0200

    some nitpicking

commit 469dba3
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Wed May 10 21:08:12 2023 +0200

    wording `26-descent`
@fredrik-bakke fredrik-bakke mentioned this pull request Jun 4, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
fix oeis
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@fredrik-bakke @EgbertRijke @VojtechStep