Can't manage to build dependency graph in Leanblueprint

Stream: new members

[Rik Heurter]

I'm currently formalising a part of my bachelor thesis in Lean (as part of my bachelor thesis) and I can't manage to get the dependency graph to build. Specifically in github actions the "Check declarations mentioned in the blueprint exist in Lean code." fails

i.e. Line 92 to 94 from the blueprint.yml workflow fail:

- name: Check declarations mentioned in the blueprint exist in Lean code
        run: |
            ~/.elan/bin/lake exe checkdecls blueprint/lean_decls

Thus I thought to run

lake build
leanblueprint checkdecls

which outputs the following:

BscThesisFormalisation.theorem2_2.EQUIOptimal is missing.
BscThesisFormalisation.definitions.coreSpace is missing.
BscThesisFormalisation.definitions.myConcave is missing.
BscThesisFormalisation.definitions.Sublinear is missing.
BscThesisFormalisation.definitions.SpeedUpFunction is missing.
BscThesisFormalisation.definitions.RateMatrix is missing.
BscThesisFormalisation.definitions.InvariantDistribution is missing.
BscThesisFormalisation.definitions.MeanResponseTime is missing.
BscThesisFormalisation.definitions.Policy is missing.
BscThesisFormalisation.definitions.SchedulePolicy is missing.
BscThesisFormalisation.lemma2_1 is missing.
Command 'lake exe checkdecls blueprint/lean_decls' returned non-zero exit status 1.

I have already looked at FLT project and Sphere eversion and see no more mayor differences in setup.

Code for reproduction:

git clone https://github.com/RikHeurter/LeanBscThesisFormalisation.git
cd LeanBscThesisFormalisation
lake build
leanblueprint checkdecls

(Warning takes ages!)

Does anybody know what I am doing wrong? My code is located at my github and is based on the Leanproject template

Furthermore lake/lean version is:
Lake version 5.0.0-045d07d (Lean version 4.19.0-rc3)
And leanblueprint version is:
leanblueprint, version 0.0.17

P.s.
This is my first time asking for help with code/computer science problems thus any feedback on what I should change to get a better answer is desired.

[Yaël Dillies]

Welcome! :wave: If you want to try things locally, you need to run the previous workflow steps too, in particular the one generating the documentation since this is what checkdecls uses to determine whether something exists

[Rémy Degenne]

BscThesisFormalisation.definitions.coreSpace is missing. tells you that there is no such declaration in your code, and that's true. There is a coreSpace in the file BscThesisFormalisation.definitions.lean but it is not in the namespace BscThesisFormalisation.definitions.
The issue seems to be that you are confusing file paths and namespaces, which are different things.

[Rémy Degenne]

So instead of \lean{BscThesisFormalisation.definitions.coreSpace}, write \lean{coreSpace} in your blueprint file.

[Rik Heurter]

Rémy Degenne said:

BscThesisFormalisation.definitions.coreSpace is missing. tells you that there is no such declaration in your code, and that's true. There is a coreSpace in the file BscThesisFormalisation.definitions.lean but it is not in the namespace BscThesisFormalisation.definitions.
The issue seems to be that you are confusing file paths and namespaces, which are different things.

Thanks! I got it to work now! Been spending 3-4 hours on figuring out what was going wrong.