Skip to content

Commit

Permalink
chore: update links
Browse files Browse the repository at this point in the history
  • Loading branch information
plt-amy committed Jul 19, 2024
1 parent 50ea36c commit 417e7ec
Show file tree
Hide file tree
Showing 9 changed files with 18 additions and 28 deletions.
14 changes: 7 additions & 7 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Thanks for taking the time to contribute!
This file holds the conventions we use around the codebase, but they're
guidelines, and not strict rules: If you're unsure of something, hop on
[the Discord](https://discord.gg/Zp2e8hYsuX) and ask there, or open [a
discussion thread](https://github.com/plt-amy/1lab/discussions)
discussion thread](https://github.com/the1lab/1lab/discussions)
if that's more your style.

## General guidelines
Expand All @@ -28,7 +28,7 @@ of the "highlight" classes, which have names corresponding to each of the
icons in [`support/web/highlights`]. These **should** use `:::`-fenced
divs:

[`support/web/highlights`]: https://github.com/plt-amy/1lab/blob/main/support/web/highlights
[`support/web/highlights`]: https://github.com/the1lab/1lab/blob/main/support/web/highlights

::: warning
Warning text goes here.
Expand Down Expand Up @@ -76,7 +76,7 @@ be referred to in prose using `` `name`{.Agda} `` (an inline code block
with class `Agda`). The [HoTT book comparison] uses this feature
extensively.

[HoTT book comparison]: https://github.com/plt-amy/1lab/blob/main/src/HoTT.lagda.md
[HoTT book comparison]: https://github.com/the1lab/1lab/blob/main/src/HoTT.lagda.md

If the definition does not naturally appear in the code, the following
idiom can be used. The implementation of identifier links prevents their
Expand Down Expand Up @@ -105,7 +105,7 @@ recommended way of working out whether or not a diagram renders
correctly is to actually build the website, since that lets you see
whether or not the image has a reasonable size in the page.

[These LaTeX packages]: https://github.com/plt-amy/1lab/blob/main/default.nix#L18-L27
[These LaTeX packages]: https://github.com/the1lab/1lab/blob/main/default.nix#L18-L27

Diagrams are compiled if they appear in a *fenced* code block with class
`quiver`. Accordingly, most of us use [q.uiver.app](https://q.uiver.app)
Expand All @@ -126,7 +126,7 @@ Note that the preamble is not directly loadable using Quiver's macros
functionality since it relies on `\definealphabet`, which is implemented
separately since it requires a shim to work on KaTeX.

[the preamble]: https://github.com/plt-amy/1lab/blob/main/src/preamble.tex
[the preamble]: https://github.com/the1lab/1lab/blob/main/src/preamble.tex

## The structure of a page

Expand Down Expand Up @@ -165,7 +165,7 @@ general structure:
A perfect example of these guidelines is [`Order.Semilattice.Free`],
since it has four different import blocks.

[`Order.Semilattice.Free`]: https://github.com/plt-amy/1lab/blob/main/src/Order/Semilattice/Free.lagda.md
[`Order.Semilattice.Free`]: https://github.com/the1lab/1lab/blob/main/src/Order/Semilattice/Free.lagda.md

## Agda code style

Expand All @@ -175,7 +175,7 @@ an equational reasoning block, anything between `⟨_⟩` does not count for
the line length limit, since those spans can be removed by the user.
(example: the [dual of the modular law] reaches column 136!)

[dual of the modular law]: https://github.com/plt-amy/1lab/blob/main/src/Cat/Allegory/Reasoning.lagda.md#L110
[dual of the modular law]: https://github.com/the1lab/1lab/blob/main/src/Cat/Allegory/Reasoning.lagda.md#L110

Types **should** be defined directly in `Type _`, if possible, then
later shown to be of a particular truncation level. This rule **may** be
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
[![Discord](https://img.shields.io/discord/914172963157323776?label=Discord&logo=discord)](https://discord.gg/Zp2e8hYsuX)
[![Build 1Lab](https://github.com/plt-amy/1lab/actions/workflows/build.yml/badge.svg)](https://github.com/plt-amy/1lab/actions/workflows/build.yml)
[![Build 1Lab](https://github.com/the1lab/1lab/actions/workflows/build.yml/badge.svg)](https://github.com/the1lab/1lab/actions/workflows/build.yml)

# [1Lab](https://1lab.dev)

Expand Down
6 changes: 3 additions & 3 deletions package.json
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@
},
"repository": {
"type": "git",
"url": "git+https://github.com/plt-amy/1lab.git"
"url": "git+https://github.com/the1lab/1lab.git"
},
"author": "Amélia Liao et. al.",
"license": "AGPL-3.0",
"bugs": {
"url": "https://github.com/plt-amy/1lab/issues"
"url": "https://github.com/the1lab/1lab/issues"
},
"homepage": "https://github.com/plt-amy/1lab#readme",
"homepage": "https://github.com/the1lab/1lab#readme",
"devDependencies": {
"@types/d3": "^7.1.0",
"d3": "^7.4.4",
Expand Down
2 changes: 1 addition & 1 deletion src/Authors.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ themselves! Try to follow the format of existing profiles [in the source
file], and keep the description short. Don't forget to mention your
pronouns.

[in the source file]: https://github.com/plt-amy/1lab/blob/main/src/Authors.lagda.md?plain=1
[in the source file]: https://github.com/the1lab/1lab/blob/main/src/Authors.lagda.md?plain=1

<!-- KEEP THIS SVG HERE -->

Expand Down
4 changes: 2 additions & 2 deletions src/index.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ work takes place on [GitHub], but ongoing discussion happens on
[Discord]. We welcome all contributions, though we would kindly ask that
anyone submitting a substantial change discuss it on Discord first.

[GitHub]: https://github.com/plt-amy/1lab
[GitHub]: https://github.com/the1lab/1lab
[Discord]: https://discord.gg/eQDNM26uKP
[authors]: Authors.html

Expand Down Expand Up @@ -208,7 +208,7 @@ their fundamental importance:
[KaTeX]: https://katex.org

[fast-fuzzy]: https://www.npmjs.com/package/fast-fuzzy
[our GitHub]: https://github.com/plt-amy/1lab/tree/main/support/web/js
[our GitHub]: https://github.com/the1lab/1lab/tree/main/support/web/js

## Other resources

Expand Down
12 changes: 1 addition & 11 deletions support/shake/README.md
Original file line number Diff line number Diff line change
@@ -1,16 +1,6 @@
# 1lab-shake & agda-typed-html
# 1lab-shake

Haskell commands used for building the 1Lab.

**1lab-shake**: Our Shakefile. (main-is: `Main.hs`)

**agda-typed-html**: Wrapper around Agda which builds HTML output with
type information on every link. (main-is: `Wrapper.hs`).

## Install

Use nix:

```
nix-env -if https://github.com/plt-amy/1lab/archive/refs/heads/main.tar.gz -A agda-typed-html
```
2 changes: 1 addition & 1 deletion support/shake/app/Shake/Recent.hs
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ blazeCommit baseUrl (Commit author subject hash date changes) = do

H.div ! A.class_ "commit" $ do
H.a
! A.href ("https://github.com/plt-amy/1lab/commit/" <> H.preEscapedTextValue hash)
! A.href ("https://github.com/the1lab/1lab/commit/" <> H.preEscapedTextValue hash)
! A.class_ "commit-subject"
$ H.text subject
H.span ! A.class_ "commit-author-date" $ do
Expand Down
2 changes: 1 addition & 1 deletion support/web/js/theme.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ document.addEventListener("DOMContentLoaded", () => {

line.parentElement!.insertBefore(
<div id="controls">
<Button icon="github" label="Link to source" click={`https://github.com/plt-amy/1lab/blob/${links.source}`} />
<Button icon="github" label="Link to source" click={`https://github.com/the1lab/1lab/blob/${links.source}`} />
<Button icon="all-pages" label="View all pages" click={`${links.baseURL}/all-pages.html`} />

<div class="dropdown">
Expand Down
2 changes: 1 addition & 1 deletion support/web/template.html
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ <h3 class="Agda" style="margin-top: 0; margin-bottom: 0; white-space: pre;">
<a href="$base-url$/">back to index</a> <br />
$endif$
<a href="all-pages.html">view all pages</a> <br />
<a href="https://github.com/plt-amy/1lab/blob/$source$">link to source</a> <br />
<a href="https://github.com/the1lab/1lab/blob/$source$">link to source</a> <br />
</div>
</noscript>

Expand Down

0 comments on commit 417e7ec

Please sign in to comment.