doc-gen4 failure on updating dependencies

Stream: lean4

[Chris Henson]

If I create a new package with lake and follow the instructions from the doc-gen4 repo, I get the following error:

chenson@pop-os:~/git$ lake new docs_mwe
chenson@pop-os:~/git$ cd docs_mwe/
chenson@pop-os:~/git/docs_mwe$ vim lakefile.lean
chenson@pop-os:~/git/docs_mwe$ lake -R -Kenv=dev update
«doc-gen4»: cloning https://github.com/leanprover/doc-gen4 to './.lake/packages/doc-gen4'
warning: «doc-gen4»: ignoring dependency manifest because it failed to load: ./.lake/packages/doc-gen4/lake-manifest.json: unknown manifest version '"1.0.0"'
MD4Lean: cloning https://github.com/acmepjz/md4lean to './.lake/packages/MD4Lean'
UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic to './.lake/packages/UnicodeBasic'
Cli: cloning https://github.com/mhuisi/lean4-cli to './.lake/packages/Cli'
error: ./.lake/packages/MD4Lean/lakefile.lean:12:53: error: function expected at
  FetchM
term has type
  ?m.155
error: ./.lake/packages/MD4Lean/lakefile.lean:25:37: error: function expected at
  FetchM
term has type
  ?m.197
warning: ./.lake/packages/MD4Lean/lakefile.lean:43:11: warning: declaration uses 'sorry'
error: ./.lake/packages/MD4Lean/lakefile.lean: package configuration has errors

This is what lakefile.lean looks like, everything else untouched:

import Lake
open Lake DSL

-- added this based on doc-gen4 instructions
meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

package «docs_mwe» where
  -- add package configuration options here

lean_lib «DocsMwe» where
  -- add library configuration options here

@[default_target]
lean_exe «docs_mwe» where
  root := `Main

[Henrik Böving]

Most likely using an outdated lean version

[Mauricio Collares]

(i.e., please paste the contents of lean-toolchain as well)

[Chris Henson]

This is what I'm using:

chenson@pop-os:~/git/docs_mwe$ lake --version
Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)
chenson@pop-os:~/git/docs_mwe$ cat lean-toolchain
stable

I use the nix package for elan, could it maybe be a bit outdated?

[Mauricio Collares]

stable means "whatever was the stable version when you first downloaded it, unless you explicitly updated it by running elan update stable". It's best to look at what doc-gen4 has in its lean-toolchain file and copy that explicitly

[Mauricio Collares]

(this behavior will change in a future version of elan, if I understand correctly)

[Mauricio Collares]

leanprover/lean4:v4.9.0-rc1 is what doc-gen is using (though probably you should go with leanprover/lean4:v4.9.0-rc3 since not much changes between release candidates and you get a few bugfixes for free)

[Chris Henson]

Thanks, all good now! I didn't understand the meaning of stable there.