Zulip Chat Archive

Stream: mathlib4

Topic: using binport only

Jakob von Raumer (Jul 14 2022 at 14:55):

I want to use the binported .oleans in a project of mine. I added 

require mathlib3port from git "https://github.com/leanprover-community/mathlib3port"

to my lake file, and tried

import Mathbin.AlgebraicGeometry.Scheme

#lookup3 algebraic_geometry.Scheme
#check AlgebraicGeometry.Scheme

as recommended by the mathport readme, but all I get is a unknown package 'Mathlib' on the import and it doesn't seem to use the oleans but instead wants to load the synported files (?). What am I doing wrong?

Alexander Bentkamp (Jul 14 2022 at 15:08):

Try import Mathbin instead. See also our discussion here:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unknown.20package.20Mathlib

Alexander Bentkamp (Jul 14 2022 at 15:10):

I don't know if this should be fixed in the mathport readme or in lake. But one of them must be wrong I think :-)

Alexander Bentkamp (Jul 14 2022 at 15:10):

@Mac @Gabriel Ebner

Alexander Bentkamp (Jul 14 2022 at 15:15):

Why do you think it's using the synported files? Maybe because when you click on the import you land in the synported files? I think that's intended and you are just being redirected there although internally the binport is used. That's what's happening for me at least.

Mac (Jul 14 2022 at 16:11):

The binported oleans (e.g., Mathbin.AlgebraicGeometry.Scheme) import Mathlib and will thus break if Mathlib is not built and on the LEAN_PATH. The binported mathlib package (e.g., mathlib3port) does require mathlib, so Lake knows to add mathlib's olean directory to LEAN_PATH. However, Lake only builds modules on-demand. That is, when they are imported. Lake determines this by processing a module's header (i.e., the imports at the top of the file) to know what imports a given module (e.g., your test code) makes. Since you only import Mathbin.AlgebraicGeometry.Scheme, that is all Lake ensures is built. And since that file only has an olean and no source file, Lake is unable to determine its imports to build them. Thus, Mathlib does not get built, which causes the error here. To fix this, you need to import Mathlib in your test file or import a file that syntatically imports Mathlib (e.g., Mathbin).

Jakob von Raumer (Jul 14 2022 at 19:58):

Thanks! That should do it, I'll test it tomorrow

Jakob von Raumer (Jul 14 2022 at 20:10):

Still the same errors... it also gives me warning: extraDepTarget has been deprecated. Try to use a custom target or raise an issue about your use case., is that related?

Jakob von Raumer (Jul 14 2022 at 20:13):

Oh it seems Mathlib just throws errors (on nightly 7-12)

Jakob von Raumer (Jul 14 2022 at 20:22):

Ah no, the error message has changed, it's now object file './lean_packages/mathlib/build/lib/Mathlib.olean' of module Mathlib does not exist. :thinking:

Jakob von Raumer (Jul 14 2022 at 20:27):

I'm confused. I can clone and build mathlib4 with nightly 7-12 without errors, but if I import it via lake with a toolchain bound to the same Lean version, it throws errors concerning Syntax vs TSyntax which suggests it uses the wrong Lean version

Arthur Paulino (Jul 14 2022 at 20:32):

Did you have a different version of the dependency already downloaded? In that case, try running lake update

Jakob von Raumer (Jul 14 2022 at 20:38):

I did try lake update... Should I remove mathlib4 from my dependencies? They currently looked like this:

require mathlib from git "https://github.com/leanprover-community/mathlib4"

require mathlib3port from git "https://github.com/leanprover-community/mathlib3port"

Jakob von Raumer (Jul 14 2022 at 20:40):

Maybe I should try removing the lake_packages folder by hand

Jakob von Raumer (Jul 14 2022 at 20:42):

Neither lake update nor removing lake_packages nor removing mathlib from the lake file helped :confused:

Jakob von Raumer (Jul 14 2022 at 20:44):

If I open the mathlib file that throws the error it compiles just fine

Jakob von Raumer (Jul 14 2022 at 20:45):

This is the full first error:

info: > LEAN_PATH=./lean_packages/mathlib3port/build/lib:./build/lib:./lean_packages/mathlib/build/lib:./lean_packages/lean3port/build/lib LD_LIBRARY_PATH=/home/javra/.elan/toolchains/leanprover--lean4---nightly-2022-07-12/lib:./lean_packages/mathlib3port/build/lib:./build/lib:./lean_packages/mathlib/build/lib:./lean_packages/lean3port/build/lib:./lean_packages/mathlib/build/lib /home/javra/.elan/toolchains/leanprover--lean4---nightly-2022-07-12/bin/lean ./lean_packages/mathlib/././Mathlib/Tactic/RestateAxiom.lean -R ./lean_packages/mathlib/./. -o ./lean_packages/mathlib/build/lib/Mathlib/Tactic/RestateAxiom.olean -i ./lean_packages/mathlib/build/lib/Mathlib/Tactic/RestateAxiom.ilean -c ./lean_packages/mathlib/build/ir/Mathlib/Tactic/RestateAxiom.c
error: stdout:
./lean_packages/mathlib/././Mathlib/Util/LibraryNote.lean:27:40: error: invalid field 'isStrLit?', the environment does not contain 'Lean.TSyntax.isStrLit?'
  title
has type
  TSyntax `str
error: external command /home/javra/.elan/toolchains/leanprover--lean4---nightly-2022-07-12/bin/lean exited with status 1

Arthur Paulino (Jul 14 2022 at 21:17):

What are the dependencies of those packages? Are they all using the same toolchain?

Jakob von Raumer (Jul 14 2022 at 21:59):

No, mathlib4 uses 07-12 and mathlib3port uses 06-13, so there might be some real incompatibility to the current lean :disappointed:

Arthur Paulino (Jul 14 2022 at 22:35):

You could try to find an older mathlib4 commit that uses that same toolchain, or something close enough to avoid conflicts

Mac (Jul 14 2022 at 23:02):

Jakob von Raumer said:

No, mathlib4 uses 07-12 and mathlib3port uses 06-13, so there might be some real incompatibility to the current lean :disappointed:

Yeah, you should be using the 06-13 nightly if you want to use Mathbin

Mac (Jul 14 2022 at 23:04):

You don't need to figure out what mathlib it requires, mathbin already specifies that. Simply require'ing mathlib3port and importing Mathlib should be enough.

Jakob von Raumer (Jul 15 2022 at 07:22):

Rest of the project needs TSyntax unfortunately, so I'll have to wait for the lean version bump (or do it myself :grinning: )

Gabriel Ebner (Jul 15 2022 at 07:54):

Yes, the Lean version needs to match exactly. The mathport releases contain the oleans after all. It's already a wonder if the source code compiles with two different Lean versions, binary compatibility is pretty much a lost cause.

Thomas Murrills (Sep 27 2022 at 02:47):

I have the same goal (use just binported mathlib files in a lean 4 project) and I'm also running into a bit of a wall with this. I've tried lake update and lake build, but upon having import Mathlib in my project, I get a very long error:

Long Error

Any idea what could be going on? I have require mathlib3port from git "https://github.com/leanprover-community/mathlib3port" in my lakefile, and import Mathlib at the top of my top-level project-named lean file. (I'm not sure if I'm structuring that correctly; just starting out with lean!)

And @Gabriel Ebner , when you say the lean version needs to match, do you mean that the lean version specified in the leanpkg.toml file needs to match the version used by mathlib3port?

Gabriel Ebner (Sep 27 2022 at 03:14):

Yeah that looks like a version mismatch.

Thomas Murrills (Sep 27 2022 at 03:24):

Ok, thanks! I'm actually having a bit of trouble fixing it, though. This suggests I use leanpkg configure, but I get the following error:

error: toolchain 'leanprover/lean4:nightly-2022-09-25' does not have the binary /Users/thomas/.elan/toolchains/leanprover--lean4---nightly-2022-09-25/bin/leanpkg

Perhaps I've chosen the wrong lean_version string (which I've naively set to "leanprover/lean4:nightly-2022-09-13")...?

Gabriel Ebner (Sep 27 2022 at 03:32):

Leanpkg is long obsolete. I'd try the following:

rm -rf lean_packages
lake update
cp lean_packages/mathlib/lean-toolchain .

Thomas Murrills (Sep 27 2022 at 03:41):

Hmm, thanks, that definitely did something! Now, with "leanprover/lean4:nightly-2022-09-13" as my lean_version, I get an error starting with "/Users/thomas/.elan/toolchains/leanprover--lean4---nightly-2022-09-11/bin/lake print-paths Init Mathlib failed" instead, which I'll count as progress. Do you know how I might find the correct version to use here?

Mario Carneiro (Sep 27 2022 at 03:42):

what is this lean_version field? AFAIK lake doesn't use that, it uses a lean-toolchain file at the root

Mario Carneiro (Sep 27 2022 at 03:43):

you should use the same lean-toolchain version present in the version of mathlib4 you are using

Thomas Murrills (Sep 27 2022 at 03:45):

Oh, maybe that's my problem. The lean_version field is in leanpkg.toml. Is that whole file obselete/unneeded now? (I may have been following an out-of-date guide...)

Mario Carneiro (Sep 27 2022 at 03:45):

the whole file is unused

Thomas Murrills (Sep 27 2022 at 03:45):

gotcha, thanks!

Thomas Murrills (Sep 27 2022 at 03:45):

let's see if the lean-toolchain thing works...

Mario Carneiro (Sep 27 2022 at 03:45):

lake gets its data from lakefile.lean and lean-toolchain

Thomas Murrills (Sep 27 2022 at 03:51):

Ok, it looks like my leantoolchain matches mathlib3port's toolchain (leanprover/lean4:nightly-2022-09-11) but I'm still getting what seems to me to be basically the same message. Here it is again in case it's slightly different:

Long Error

Thomas Murrills (Sep 27 2022 at 03:52):

Somehow the error got much longer, so that's just a sample. I suppose it must be a different error, on some level...

Mario Carneiro (Sep 27 2022 at 03:53):

mathlib4, not mathlib3port

Mario Carneiro (Sep 27 2022 at 03:53):

what's in your lean_packages/manifest.json file?

Thomas Murrills (Sep 27 2022 at 03:54):

Oh, ok, an earlier message suggested this: "simply require'ing mathlib3port and importing Mathlib should be enough" so that's what I was going off of!

Thomas Murrills (Sep 27 2022 at 03:54):

Let's find out...

Thomas Murrills (Sep 27 2022 at 03:55):

Here it is:

manifest.json

Mario Carneiro (Sep 27 2022 at 03:57):

You have the latest commit of std4 there, which is on 09-26, so I don't think it will play well with mathlib3port from 09-11

Thomas Murrills (Sep 27 2022 at 03:58):

Hmm, that's strange. I did just rm -rf this.

Mario Carneiro (Sep 27 2022 at 03:58):

well mathlib3port hasn't been released in a while

Mario Carneiro (Sep 27 2022 at 03:58):

so it's probably not your fault

Thomas Murrills (Sep 27 2022 at 04:00):

Huh, ok. Is std coming...via mathlip3port, so to speak? Or from somewhere else? Is there any way to force it to play nice?

Mario Carneiro (Sep 27 2022 at 04:00):

lean4 -> std4 -> mathlib4 -> mathlib3port

Thomas Murrills (Sep 27 2022 at 04:00):

I see

Mario Carneiro (Sep 27 2022 at 04:01):

I think you are likely to have best results using the 09-26 nightly

Thomas Murrills (Sep 27 2022 at 04:01):

I would have thought using a 2022-9-11 lean toolchain would have prevented that, though?

Mario Carneiro (Sep 27 2022 at 04:01):

since mathlib3port doesn't make much use of lean features

Thomas Murrills (Sep 27 2022 at 04:02):

Ok, that's what I started with—but then is there a way to make it work with mathlib binaries?

Mario Carneiro (Sep 27 2022 at 04:02):

building std4 on 09-11 is not going to work, it uses features from the future

Mario Carneiro (Sep 27 2022 at 04:02):

the alternative is to check out an old version of the dependencies, that is, use whatever version there was on 09-11

Thomas Murrills (Sep 27 2022 at 04:03):

I think that's what I'd like to do if it's the only way to use the mathlib binaries—if there's another way I'm all ears though

Mario Carneiro (Sep 27 2022 at 04:04):

std4 -> 6488a2afeb62fb4c781d26d629796480c8270b2f
mathlib4 -> dd1ecc5d3aefab6a83767079c7d020f4aa254a24

Mario Carneiro (Sep 27 2022 at 04:04):

put those in your manifest

Thomas Murrills (Sep 27 2022 at 04:05):

oo ok great! (Aside: I also would have naively thought specifying a toolchain date would have prevented using features from the future, though. my lean-toolchain is leanprover/lean4:nightly-2022-09-11, so I'd expect it to only use things from then or earlier in the "lean4 ->" stage.)

Mario Carneiro (Sep 27 2022 at 04:05):

yeah, lake isn't very good at managing the lean toolchain version

Mario Carneiro (Sep 27 2022 at 04:06):

it just uses whatever you specify and hopes for the best

Thomas Murrills (Sep 27 2022 at 04:06):

ah gotcha lol

Thomas Murrills (Sep 27 2022 at 04:06):

Ok, is it lake update now?

Mario Carneiro (Sep 27 2022 at 04:07):

Asking for the versions to match exactly is also problematic though, because there's a new version every day and maintainers can't keep up with that pace

Mario Carneiro (Sep 27 2022 at 04:07):

most of the time whatever changes there were are not relevant to the library

Mario Carneiro (Sep 27 2022 at 04:07):

lake update will update the manifest to the latest version of everything, which will undo the work you just did

Thomas Murrills (Sep 27 2022 at 04:08):

ah! I understand now haha

Thomas Murrills (Sep 27 2022 at 04:14):

ok, I've tried deleting everything but the manifest and rebuilding, but now it doesn't like any of the imports in lean_packages/std/Std.lean either...hmmm

Thomas Murrills (Sep 27 2022 at 04:16):

hmm, the lean_packages/std/lean-toolchain is still the 9-26 nightly build

Thomas Murrills (Sep 27 2022 at 04:18):

(and as far as I can tell no update has taken place; 6488a2afeb62fb4c781d26d629796480c8270b2f is still in the manifest)

Thomas Murrills (Sep 27 2022 at 04:30):

does lake actually use the manifest or is it meant to be more of a record? if it does use it, I'm not sure why this isn't working...hmmm. perhaps this can be fixed by fixing lake somehow...I'm going to investigate tomorrow :) (I also wonder if people would agree that this needs to be fixed in lake. my argument would be that the point of having versioned toolchains is to prevent breaking changes like this! :) )

Thomas Murrills (Sep 27 2022 at 04:39):

anyway thanks to both of you for all of your help so far! :) I’m not giving up…we’ll figure this out eventually!

James Gallicchio (Sep 27 2022 at 04:54):

There is some ongoing discussion (here and here) about precisely this issue... the answer isn't straightforward

Mario Carneiro (Sep 27 2022 at 04:55):

lake checks out the commit in the manifest first thing when you run lake build, at least in my experience

Mario Carneiro (Sep 27 2022 at 04:55):

but one way to be sure is to copy the manifest file, delete the lean_packages folder entirely, restore the manifest and call lake build

Mario Carneiro (Sep 27 2022 at 04:57):

(that file should really not be in the lean_packages folder)

James Gallicchio (Sep 27 2022 at 04:57):

I'm not even confident that's the case, given how I'm now observing lake changing my manifest without me asking it to. Just haven't had time to investigate why

Thomas Murrills (Sep 28 2022 at 03:53):

but one way to be sure is to copy the manifest file, delete the lean_packages folder entirely, restore the manifest and call lake build

Hmm...I moved the modified manifest.json to the top level of the project and rm -rf'd lean_packages and build, then called lake build. This generated a new manifest inside the created lean_packages, and still used a std that had a 9-26 toolchain, unfortunately :/

Mario Carneiro (Sep 28 2022 at 04:03):

you have to restore the manifest before calling lake build

Thomas Murrills (Sep 28 2022 at 04:03):

what does it mean to restore a manifest?

Mario Carneiro (Sep 28 2022 at 04:03):

put the file you copied back where it was

Thomas Murrills (Sep 28 2022 at 04:03):

it was in lean_packages, though

Mario Carneiro (Sep 28 2022 at 04:04):

so that nuking the lean_packages folder doesn't also nuke your changes

Mario Carneiro (Sep 28 2022 at 04:05):

That is, you want to delete everything in lean_packages except the manifest that is the only record that you are interested in something other than the latest version

Thomas Murrills (Sep 28 2022 at 04:06):

right, ok; I had tried that last night already, as it happens

Thomas Murrills (Sep 28 2022 at 04:06):

what I hadn't tried was keeping it outside the folder

Mario Carneiro (Sep 28 2022 at 04:07):

if you run lake build with a lean_packages folder that only has the modified manifest in it and nothing else, in my experience lake will respect it and download the right versions

Thomas Murrills (Sep 28 2022 at 04:07):

I did find something weird playing around (well, weird since I don't know what it means, lol): changing inputRev in the manifest seems to successfully change the std that gets cloned to one with a 9-11 toolchain

Thomas Murrills (Sep 28 2022 at 04:07):

gotcha; I just tried it again, and unfortunately deleting everything but the manifest in lean_packages didn't work :/

Mario Carneiro (Sep 28 2022 at 04:08):

I usually update the "rev" field, this should make lake download the version

Thomas Murrills (Sep 28 2022 at 04:09):

Yeah, that's what I had been trying already

Thomas Murrills (Sep 28 2022 at 04:09):

(which wasn't working, so I tried changing the inputRev as well)

Mario Carneiro (Sep 28 2022 at 04:09):

and it's updating the rev?

Thomas Murrills (Sep 28 2022 at 04:10):

so to be clear, if this is in my manifest

{"url": "https://github.com/leanprover/std4",
   "rev": "6488a2afeb62fb4c781d26d629796480c8270b2f",
   "name": "std",
   "inputRev": "main"}

it doesn't work; clones a version of std with lean-toolchain leanprover/lean4:nightly-2022-09-26, which isn't consistent with rev 6488a2afeb62fb4c781d26d629796480c8270b2f of std on github.

Mario Carneiro (Sep 28 2022 at 04:12):

It is downloading 6488a2 though?

Thomas Murrills (Sep 28 2022 at 04:13):

no, it's not; if it were, the lean-toolchain in std ould be for 9-11

Mario Carneiro (Sep 28 2022 at 04:13):

what version is it?

Mario Carneiro (Sep 28 2022 at 04:13):

it says "downloading version XYZ" when it goes to github

Thomas Murrills (Sep 28 2022 at 04:14):

hmm, do I need a verbose option for lake build or something? currently it just says info: cloning https://github.com/leanprover/std4 to ./lean_packages/std

Mario Carneiro (Sep 28 2022 at 04:15):

specifically, I get a message like

info: updating ./lean_packages/std to revision 6488a2afeb62fb4c781d26d629796480c8270b2f

when I change the manifest and run lake build

Thomas Murrills (Sep 28 2022 at 04:15):

actually, ok, something else very weird: it updates the manifest without me touching it

Thomas Murrills (Sep 28 2022 at 04:15):

and you have "inputRev": "main" as well?

Mario Carneiro (Sep 28 2022 at 04:15):

yes

Thomas Murrills (Sep 28 2022 at 04:16):

hmmmm

Mario Carneiro (Sep 28 2022 at 04:17):

oh, no when I delete the directory entirely it doesn't report the revision

Mario Carneiro (Sep 28 2022 at 04:18):

but if you go inside lean_packages/std/ and run git rev-parse HEAD it will report the revision

Thomas Murrills (Sep 28 2022 at 04:18):

hmm yep, that gives me 52c2324923b7f83e4e9b82ca9c8284f7a86bd3e8

Mario Carneiro (Sep 28 2022 at 04:19):

what happens if you git checkout 6488a2afeb62fb4c781d26d629796480c8270b2f and change the manifest to match?

Mario Carneiro (Sep 28 2022 at 04:19):

this is really weird

Thomas Murrills (Sep 28 2022 at 04:20):

ok VERY strange

Thomas Murrills (Sep 28 2022 at 04:21):

i successfully checked out:

Previous HEAD position was 52c2324 feat: use simp trace support in simpNF linter
HEAD is now at 6488a2a chore: update nightly 09-11 (#7)

cd'd back up to the project level, changed the rev in the manifest and made sure to save it; lake build then changed the manifest back as I watched :sweat_smile:

Mario Carneiro (Sep 28 2022 at 04:22):

what's in the lakefile.lean?

Thomas Murrills (Sep 28 2022 at 04:22):

lakefile.lean

Thomas Murrills (Sep 28 2022 at 04:23):

(The only thing I changed/added was the require statement)

Thomas Murrills (Sep 28 2022 at 04:24):

now, for whatever reason, if I change inputRev (and maybe this is obvious; I don't yet know what inputRev means) I get the messages

warning: std: revision `6488a2afeb62fb4c781d26d629796480c8270b2f` listed in manifest does not match `main` listed in the configuration file; you may wish to run `lake update` to update
info: updating ./lean_packages/std to revision 6488a2afeb62fb4c781d26d629796480c8270b2f

Thomas Murrills (Sep 28 2022 at 04:25):

and then indeed the revision is reported by git rev-parse HEAD as 6488a2afeb62fb4c781d26d629796480c8270b2f. however, nothing works this time either, because of the mismatch between the configuration files

Mario Carneiro (Sep 28 2022 at 04:26):

inputRev means the revision specified in the input i.e. in the lakefile

Mario Carneiro (Sep 28 2022 at 04:27):

because the only thing better than global mutable state is having that state in two places that have to match

Thomas Murrills (Sep 28 2022 at 04:27):

haha yes

Thomas Murrills (Sep 28 2022 at 04:28):

so I'm guessing something's up with how lake uses

@[defaultTarget]
lean_exe moonshine {
  root := `Main
}

?

Thomas Murrills (Sep 28 2022 at 04:32):

because if I sort of..."disconnect" std's manifest entry from its inputRev, I don't get the weird behavior. so somehow I'm guessing...if lake build sees main, it decides to update the manifest entry and std, presumably in accordance with something determined by what it saw there, i.e. main?

Thomas Murrills (Sep 28 2022 at 04:36):

and for whatever it's worth, if i just straight up delete the inputRev key from the std entry in the manifest, I still get an error on import Mathlib, but it's this:

Long Error

Mario Carneiro (Sep 28 2022 at 04:38):

So this code looks pretty suspicious

      let shouldUpdate :=
        match entry.inputRev?, depEntry.inputRev? with
        | none,     none     => entry.rev != depEntry.rev
        | none,     some _   => false
        | some _,   none     => false
        | some rev, some dep => rev = dep ∧ entry.rev ≠ depEntry.rev
      let contributors := entry.contributors.insert depPkg.name depEntry.toPersistentPackageEntry
      modify (·.insert {entry with contributors, shouldUpdate})

Thomas Murrills (Sep 28 2022 at 04:38):

oooo

Mario Carneiro (Sep 28 2022 at 04:39):

Note that the function there was passed a shouldUpdate flag which isn't being checked here

Mario Carneiro (Sep 28 2022 at 04:39):

shouldUpdate is false when running lake build

Mario Carneiro (Sep 28 2022 at 04:40):

From the looks of that match, it seems that it decides to update in response to a mismatch of rev fields in a dependency

Mario Carneiro (Sep 28 2022 at 04:41):

cc: @Mac

Thomas Murrills (Sep 28 2022 at 05:05):

just in case it helps debug things, here's verbose output (lake -v build) for one of the "weird" instances, where inputRev is main, and where the rev is mysteriously changed from 6488a2... to 52c232.... This started with only a modified lean_packages/manifest.json and no other files.

verbose build

Thomas Murrills (Sep 28 2022 at 18:40):

One thing I'm noticing: each of the generated lean3port, mathlib, mathlib3port directories within lean_packages have their own lean_packages directories within them, containing nothing but a manifest.json file. Should the revs in this manifest be reflected at the top level as well? They seem to use rev 1f3f0630659a96756377610db656253b18a6a7ee of std, instead of either of the two that have been tried so far.

Mac (Sep 28 2022 at 20:07):

Mario Carneiro said:

From the looks of that match, it seems that it decides to update in response to a mismatch of rev fields in a dependency

Yes, that is the goal. See this comment on lake#120 for more information. I think the underlying problem is actually the one mentioned in lake#119 here.

Mario Carneiro (Sep 28 2022 at 20:12):

@Mac I don't suppose the lake dependency resolution algorithm could be documented somewhere in plain text in the documentation? It seems worth an RFC in case it's not actually doing what we want. Currently I have difficulty reading the code because I know neither what it is supposed to do nor what the invariants of the internal data structures are when processing all the dependencies.

Mac (Sep 28 2022 at 20:15):

@Mario Carneiro Yeah, this is a good idea. I definitely think that I now need to fix these bugs ASAP (hopefully by this weekend). While doing so, I can also write-up some doc on how I see it working. Feel free to also create issue requesting the docs on GitHub with anything you want to make sure I include. I can tell you the current approach is a bit haphazard as it has been mostly developed from me addressing @Gabriel Ebner 's feature requests.

Mario Carneiro (Sep 28 2022 at 20:16):

Quick question in regards to something I brought up above: why does the inputRev field exist? The input revision should presumably be in the lakefile.

Mac (Sep 28 2022 at 20:17):

@Mario Carneiro lake#85

Last updated: Dec 20 2023 at 11:08 UTC