Dax Fohl
2877196656
doc: fix broken "quickstart" and "supported editors" link ( #8785 )
...
The "supported editors" link in
https://github.com/leanprover/lean4/blob/master/doc/dev/index.md is
broken, as `setup.md` no longer exists in the repo. This PR changes the
link to point to the live Lean docs setup page at
https://docs.lean-lang.org/lean4/doc/setup.html#editing .
A similar fix for quickstart is included.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch >
2025-09-02 12:45:04 +00:00
Sebastian Ullrich
f678b40660
chore: make USE_LAKE the default ( #10016 )
2025-08-21 11:43:25 +00:00
Sebastian Ullrich
679df58329
chore: revert "chore: make USE_LAKE the default" ( #10011 )
...
Reverts leanprover/lean4#10003 , which broke the merge queue's breakage
check
2025-08-20 19:52:57 +00:00
Sebastian Ullrich
44891fe0c0
chore: make USE_LAKE the default ( #10003 )
2025-08-20 19:24:10 +00:00
Sebastian Ullrich
99dac6aec0
doc: building core with Lake ( #9547 )
2025-07-26 06:13:09 +00:00
dependabot[bot]
b1c2d851e5
chore: CI: bump lycheeverse/lychee-action from 1.9.0 to 2.0.2 ( #5959 )
...
Bumps
[lycheeverse/lychee-action](https://github.com/lycheeverse/lychee-action )
from 1.9.0 to 2.0.2.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/lycheeverse/lychee-action/releases ">lycheeverse/lychee-action's
releases</a>.</em></p>
<blockquote>
<h2>Version 2.0.2</h2>
<h2>What's Changed</h2>
<ul>
<li>Fix a typos by <a
href="https://github.com/szepeviktor "><code>@szepeviktor</code></a> in
<a
href="https://redirect.github.com/lycheeverse/lychee-action/pull/257 ">lycheeverse/lychee-action#257</a></li>
<li>Document and use correct permissions in the GitHub workflows by <a
href="https://github.com/dscho "><code>@dscho</code></a> in <a
href="https://redirect.github.com/lycheeverse/lychee-action/pull/258 ">lycheeverse/lychee-action#258</a></li>
<li>Add security policy by <a
href="https://github.com/mondeja "><code>@mondeja</code></a> in <a
href="https://redirect.github.com/lycheeverse/lychee-action/pull/259 ">lycheeverse/lychee-action#259</a></li>
</ul>
<h2>New Contributors</h2>
<ul>
<li><a
href="https://github.com/szepeviktor "><code>@szepeviktor</code></a>
made their first contribution in <a
href="https://redirect.github.com/lycheeverse/lychee-action/pull/257 ">lycheeverse/lychee-action#257</a></li>
<li><a href="https://github.com/mondeja "><code>@mondeja</code></a> made
their first contribution in <a
href="https://redirect.github.com/lycheeverse/lychee-action/pull/259 ">lycheeverse/lychee-action#259</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/lycheeverse/lychee-action/compare/v2...v2.0.2 ">https://github.com/lycheeverse/lychee-action/compare/v2...v2.0.2 </a></p>
<h2>Version 2.0.1</h2>
<h2>What's Changed</h2>
<ul>
<li>Don't remove the lychee config file by <a
href="https://github.com/dmathieu "><code>@dmathieu</code></a> in <a
href="https://redirect.github.com/lycheeverse/lychee-action/pull/255 ">lycheeverse/lychee-action#255</a></li>
<li>Bump lycheeverse/lychee-action from 1 to 2 by <a
href="https://github.com/dependabot "><code>@dependabot</code></a> in <a
href="https://redirect.github.com/lycheeverse/lychee-action/pull/252 ">lycheeverse/lychee-action#252</a></li>
<li>Fix variable name in docs by <a
href="https://github.com/kdeldycke "><code>@kdeldycke</code></a> in <a
href="https://redirect.github.com/lycheeverse/lychee-action/pull/253 ">lycheeverse/lychee-action#253</a></li>
</ul>
<h2>New Contributors</h2>
<ul>
<li><a href="https://github.com/dmathieu "><code>@dmathieu</code></a>
made their first contribution in <a
href="https://redirect.github.com/lycheeverse/lychee-action/pull/255 ">lycheeverse/lychee-action#255</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/lycheeverse/lychee-action/compare/v2...v2.0.1 ">https://github.com/lycheeverse/lychee-action/compare/v2...v2.0.1 </a></p>
<h2>Version 2.0.0</h2>
<h2>Breaking Changes</h2>
<p><strong>Note:</strong> This release improves the action's robustness
by changing default behaviors. Changes are only required if you want to
opt out of the new failure conditions. Most users won't need to modify
their existing configurations.</p>
<h3>Fail pipeline on error by default</h3>
<p>We've changed the default behavior: pipelines will now fail on broken
links automatically. This addresses user feedback that not failing on
broken links was unexpected (see [issue <a
href="https://redirect.github.com/lycheeverse/lychee-action/issues/71 ">#71</a>](<a
href="https://redirect.github.com/lycheeverse/lychee-action/issues/71 ">lycheeverse/lychee-action#71</a>)).</p>
<p><strong>What you need to do:</strong></p>
<ul>
<li>Update to version 2 of this action to apply this change.</li>
<li>Users of the <code>lychee-action@master</code> branch don't need to
make any changes, as <code>fail: true</code> has been the default there
for a while.</li>
<li>If you prefer the old behavior, explicitly set <code>fail</code> to
<code>false</code> when updating:</li>
</ul>
<pre lang="yaml"><code>- name: Link Checker
id: lychee
uses: lycheeverse/lychee-action@v2
with:
fail: false # Don't fail action on broken links
</code></pre>
<h3>Fail pipeline if no links were found</h3>
<p>Similar to the above change, we now fail the pipeline if no links are
found during a run. This helps warn users about potential configuration
issues.</p>
<p><strong>What you need to do:</strong></p>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="7cd0af4c748ad54d3568762333c189https://redirect.github.com/lycheeverse/lychee-action/issues/259 ">#259</a>)</li>
<li><a
href="71a38a3bd7https://redirect.github.com/lycheeverse/lychee-action/issues/258 ">#258</a>)</li>
<li><a
href="f141760066https://redirect.github.com/lycheeverse/lychee-action/issues/257 ">#257</a>)</li>
<li><a
href="2bb232618bhttps://redirect.github.com/lycheeverse/lychee-action/issues/255 ">#255</a>)</li>
<li><a
href="731bf1a2afhttps://redirect.github.com/lycheeverse/lychee-action/issues/253 ">#253</a>)</li>
<li><a
href="e360f3c891https://redirect.github.com/lycheeverse/lychee-action/issues/252 ">#252</a>)</li>
<li><a
href="f87f0a62997da8ec1fc4https://redirect.github.com/lycheeverse/lychee-action/issues/236 ">#236</a>)</li>
<li>Additional commits viewable in <a
href="https://github.com/lycheeverse/lychee-action/compare/v1.9.0...v2.0.2 ">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores )
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
</details>
---------
Signed-off-by: dependabot[bot] <support@github.com >
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch >
2024-11-05 10:41:16 +00:00
Markus Himmel
c237c1f9fb
feat: link LibUV ( #4963 )
2024-08-12 12:33:24 +00:00
Alok Singh
6dd502321f
chore: add parallelism fallback for macOS on build ( #4647 )
...
1 less thing to think about.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch >
2024-08-08 14:26:06 +00:00
Sebastian Ullrich
73a0c73c7c
chore: modernize build instructions ( #4032 )
...
Use `cmake --preset`, adjust and document parallelism settings
2024-05-23 10:55:07 +00:00
Joachim Breitner
2867b93d51
chore: replace shell.nix with a devShell in flake.nix ( #3717 )
...
as a side effect this pins the “old nixpkgs” revision used by CI for
release builds.
(Not that that old branch is likely to change a lot…)
2024-03-21 13:24:01 +00:00
David Thrane Christiansen
1f4359cc80
fix: broken internal links in the docs ( #3216 )
...
I deleted internal links that seemed to have the character of "TODO". I
think that the residual TODO is of little value, given that we plan a
big revamp and revision soon anyway, but I could do it some other way as
well.
2024-01-25 09:56:20 +00:00
Sebastian Ullrich
ea5b55b8f2
doc: remove Nix docs
2023-12-01 08:32:20 +00:00
Sebastian Ullrich
d2c626e158
doc: refine development manual
2022-04-05 16:03:24 +02:00
Sebastian Ullrich
c29ad9a9b3
doc: ubuntu: specify fewer versions that will become outdated anyway
2021-11-09 09:41:18 +01:00
Sebastian Ullrich
7a91c494b9
chore: submodule hints
2021-10-15 06:56:02 -07:00
Sebastian Ullrich
74b813fbcd
doc: restructure make/index.md
...
debug builds are not very interesting currently given the state of
debugging Lean code
2021-10-15 06:56:02 -07:00
Chris Lovett
3a20b6be8a
doc: add wsl setup docs and reorganize a new "dev" folder
2021-09-23 09:21:39 +02:00
Chris Lovett
1591bb1640
doc: fix msys text based on code review feedback
2021-09-10 10:07:57 +02:00
Sebastian Ullrich
917eb4d081
chore: collect stdlib compilation flags in new header
2021-08-12 07:51:50 -07:00
Sebastian Ullrich
7e78de978d
doc: further bootstrapping complications
2021-08-12 07:51:50 -07:00
Sebastian Ullrich
8175003707
doc: update links to elan
2021-04-17 16:33:23 +02:00
Sebastian Ullrich
f80147e264
doc: update dev setup editor instructions
2021-02-02 17:30:51 +01:00
Sebastian Ullrich
b0f1bfb580
doc: fix ctest advice
2020-12-29 14:42:48 -08:00
Sebastian Ullrich
ffb8e1904b
doc: Nix setup
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
e167085429
doc: remove outdated description
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
c54d51b0c9
chore: go back to previous bootstrapping scheme where the stage N+1 stdlib is created using the stage N compiler
2020-09-24 18:57:53 +02:00
mhuisi
21d176c1ea
doc: correct msys2 build instructions
2020-08-25 16:08:58 +02:00
Sebastian Ullrich
34e496d606
chore: add stage 1.5 (yes, really)
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
ff0d56da65
doc: further elaborate on elan and Emacs setup
...
/cc @leodemoura @mhuisi
2020-05-18 11:00:29 +02:00
Sebastian Ullrich
bb554930f8
doc: elaborate on elan setup
2020-05-15 21:31:23 +02:00
Sebastian Ullrich
ed9b845eaa
chore: test/update-stage0 targets with default stage
2020-05-15 11:46:38 +02:00
Sebastian Ullrich
f64a343183
doc: describe new bootstrap setup
2020-05-14 23:13:51 +02:00
Sebastian Ullrich
274e6bf931
doc: update make docs
2020-05-14 14:47:54 +02:00
Sebastian Ullrich
dda44bc47f
doc: building Lean using Nix in WSL does work reasonably well
2020-03-25 14:24:49 +01:00
Sebastian Ullrich
1756d31694
chore: update build instructions
2020-03-25 12:45:52 +01:00
Daniel Selsam
b4e285f91a
fix: dead link in doc
2020-01-02 14:36:14 +01:00
Sebastian Ullrich
5ce037b7e8
doc: document stage2&3
...
/cc @leodemoura
2019-12-16 13:32:34 +01:00
Sebastian Ullrich
21ac37378e
doc: update build docs
2019-11-29 11:23:42 +01:00
Sebastian Ullrich
cf0808c0c3
doc: update ccache docs
2019-11-25 14:09:42 +01:00
Sebastian Ullrich
49b356e591
doc: update make docs
2019-11-11 15:05:25 -08:00
Leonardo de Moura
5679a17603
doc(doc/make/index): add instructions for invoking makefile manually
2019-03-25 14:57:57 -07:00
Sebastian Ullrich
0279d29741
chore(shell/CMakeLists): add bin_lean_stage0 target
2019-03-21 13:16:34 +01:00
Sebastian Ullrich
beae045ebc
fix(CMakeLists): complete move of stage1 from src/ to build dir
2019-03-21 13:16:17 +01:00
Sebastian Ullrich
74eab92c7c
doc(doc/make/index): add some bootstrapping docs
...
@leodemoura
2019-03-18 21:50:07 +01:00
Sebastian Ullrich
2e784cd6be
doc(doc/make/emscripten): document Emscripten build
2018-04-30 18:17:16 +02:00
Nuno Lopes
a9078dd13a
fix(doc): link to MSVC build instructions
2018-02-13 10:40:53 -08:00
Nuno Lopes
59b5a4a07a
feat(build): add preliminary MSVC support
...
Still doesn't build fully, but at least Intellisense sort of works now
2018-02-06 10:11:09 -08:00
Sean Leather
ddfd52b863
fix(doc/make/index.md): link typo
2018-02-01 09:53:26 +01:00
Sebastian Ullrich
19f8bfd9eb
chore(doc/make): add platform-generic build instructions
2018-01-23 11:14:18 -08:00
