how do you install Scilean in an existing project

Stream: general

[Robert]

I set up https://github.com/lecopivo/SciLean as in the manual, but I have say another repo where I want to now call SciLean, how do I set it up in my lakefile.lean ? Like for Batteries https://github.com/leanprover-community/batteries i just had toi insert into my lakefile

require "leanprover-community" / "batteries" @ git "main"

and it worked, i tried the same for SciLean but it gave me an error. Any help?

[Ruben Van de Velde]

What did you write, exactly?

[Robert]

I wrote

require "lecopivo" / "SciLean" @ git "master"

[Ruben Van de Velde]

I wonder if that requires Reservoir support...

[Kim Morrison]

Yes, the new short require syntax requires that Reservoir has indexed the project.

@Mac Malone, can you do something to make sure that the error message in this situation is really clear? Ideally including links to reservoir, explanations about how to get something indexed by reservoir, ideally ideally even a link to the page on reservoir explaining why this project hasn't been indexed, etc.

People are always going to set up there lakefiles by copying and pasting someone elses, so this is going to be a ubiquitous failure mode.

[Kim Morrison]

Currently I get:

% lake build
error: dependency 'SciLean' not in manifest; use `lake update SciLean` to add it
% lake update SciLean
error: lecopivo/SciLean: Reservoir lookup failed: Internal server error
error: lecopivo/SciLean: could not materialize package: dependency has no explicit source and was not found on Reservoir

[Kim Morrison]

.... which is completely unactionable.

[Mac Malone]

The internal server error is not good and definitely indicates something amiss.

[Kim Morrison]

This really must print a suggestion of the

require "lecopivo" / "SciLean" @ git "master"
  from git "https://github.com/lecopivo/SciLean" @ "master"

[Kim Morrison]

although that errors as error: mathlib: package 'scilean' was required as 'SciLean'

[Mac Malone]

SciLean is indexed by Reservoir though (see here)

[Kim Morrison]

So the correct suggestion is actually

require "lecopivo" / "scilean" @ git "master"
  from git "https://github.com/lecopivo/SciLean" @ "master"

[Mac Malone]

The from git is unnecessary in this case because Reservoir does index it.

[Kim Morrison]

Okay... so what should it be printing here?

[Kim Morrison]

The reservoir failing because of the casing discrepancy?

[Mac Malone]

What you suggested initially is probably ideal for unindexed packages. The problem here is likely a Reservoir bug (indicating by the internal serve error).

[Mac Malone]

What Lake should ideally do here is special case on the response code, but it was not clear to me how to do that with curl iniitally. I think i have discovered a way in the interim, which could be used to improve this error.

[Kim Morrison]

Okay -- for unindexed packages, do you think we can get this done asap? I'm happy to cut an RC for this, we really can't leave users unable to add packages.

[Mac Malone]

Possibly? I was planning to be done for the day and on Thanksgiving vacation, but I can see if it can't hot fix this.

[Kim Morrison]

I'm not planning on cutting v4.14.0 stable until early next week anyway, so please don't interrupt any vacation plans!! (Despite me wanting to get this fixed asap, I strongly believe in defending vacations. :-)

[Mac Malone]

@Kim Morrison The internal server error you encountered seems like it was a single network failure. While that should be fixed with retries, I don't think the error @Robert encountered was yours. When I try a lakefile with

package test

require "lecopivo" / "SciLean" @ git "master"

I get:

$ lake -d private/require-test resolve-deps
info: test: no previous manifest, creating one from scratch
info: lecopivo/scilean: cloning https://github.com/lecopivo/SciLean
info: lecopivo/scilean: checking out revision '3cb99b5bb69dcbe69c694c78e364c589eca8781e'
info: updating toolchain to 'leanprover/lean4:v4.14.0-rc2'
info: restarting Lake via Elan
info: test: no previous manifest, creating one from scratch
trace: private/require-test\.\.lake\packages\scilean> git fetch --tags --force origin
error: 'SciLean' was downloaded incorrectly; you will need to manually delete 'private/require-test\.\.lake\packages\scilean': permission denied (error code: 13)
  file: private/require-test\.\.lake\packages\scilean\.git\objects\pack\pack-07df397d18640e15e0e7822b39a4535cc6b5a17e.idx
error: test: package 'scilean' was required as 'SciLean'

In which case, I believe the underlying error was just the mispelling?

[Mac Malone]

(The error message you encountered still does need improvement, though.)

[Mac Malone]

@Kim Morrison Improved error message is at lean4#6231. Feel free to suggest any changes.

[Robert]

thanks for all your help, but sorry I still dont understand how to install it, is it just that I use this line

require "lecopivo" / "SciLean" @ git "master"
  from git "https://github.com/lecopivo/SciLean" @ "master"

or something more? I tried that but it didnt work

[Robert]

any updates here @Kim Morrison @Mac Malone? I also am tagging @Tomas Skrivan since he is the owner of SciLean?

[Mac Malone]

@Robert The correct invocation should be:

require "lecopivo" / "scilean"

[Robert]

Thank you so much @Mac Malone ! it worked

[Kim Morrison]

Sorry Robert, I thought I'd replied earlier today, but apparently not. I did try out your previous attempt above, and although it didn't work right away, I thought the error messages did clearly explain what to change.