Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

npm "MODULE_NOT_FOUND" error #97

Open
AwayGithub opened this issue Dec 18, 2024 · 1 comment
Open

npm "MODULE_NOT_FOUND" error #97

AwayGithub opened this issue Dec 18, 2024 · 1 comment
Labels
question Further information is requested

Comments

@AwayGithub
Copy link

I'm trying to import Mathlib.Tactic.Ring, and I encounter this error:

`d:\Lean4\lean-4.15.0-rc1-windows\bin\lake.exe setup-file E:/Learn/LEAN/work/Main.lean Init Work Paperproof Mathlib.Data.Rat.Init Mathlib.Tactic.Linarith Mathlib.Tactic.Ring` failed:

stderr:
⚠ [5/690] Replayed BetterParser
warning: .\.\.lake/packages\Paperproof\lean\.\.\BetterParser.lean:41:3: `List.bind` has been deprecated: use `List.flatMap` instead
warning: .\.\.lake/packages\Paperproof\lean\.\.\BetterParser.lean:168:17: `List.join` has been deprecated: use `List.flatten` instead
warning: .\.\.lake/packages\Paperproof\lean\.\.\BetterParser.lean:169:54: `List.bind` has been deprecated: use `List.flatMap` instead
warning: .\.\.lake/packages\Paperproof\lean\.\.\BetterParser.lean:181:26: `List.join` has been deprecated: use `List.flatten` instead
✖ [600/690] Building proofwidgets/widgetJsAll
trace: .\.\.lake/packages\proofwidgets\widget> npm.cmd clean-install
trace: stderr:
node:internal/modules/cjs/loader:1228
  throw err;
  ^

Error: Cannot find module 'e:\Learn\LEAN\work\.lake\packages\proofwidgets\widget\node_modules\npm\bin\npm-prefix.js'
    at Module._resolveFilename (node:internal/modules/cjs/loader:1225:15)
    at Module._load (node:internal/modules/cjs/loader:1051:27)
    at Function.executeUserEntryPoint [as runMain] (node:internal/modules/run_main:174:12)
    at node:internal/main/run_main_module:28:49 {
  code: 'MODULE_NOT_FOUND',
  requireStack: []
}

Node.js v20.18.0
node:internal/modules/cjs/loader:1228
  throw err;
  ^

Error: Cannot find module 'e:\Learn\LEAN\work\.lake\packages\proofwidgets\widget\node_modules\npm\bin\npm-cli.js'
    at Module._resolveFilename (node:internal/modules/cjs/loader:1225:15)
    at Module._load (node:internal/modules/cjs/loader:1051:27)
    at Function.executeUserEntryPoint [as runMain] (node:internal/modules/run_main:174:12)
    at node:internal/main/run_main_module:28:49 {
  code: 'MODULE_NOT_FOUND',
  requireStack: []
}

Node.js v20.18.0
error: external command 'npm.cmd' exited with code 1
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed

I don't know if the problem is with my installation of the mathlib library or with Node.js. I‘d be grateful if someone offer to help!

@Vtec234 Vtec234 added the question Further information is requested label Dec 20, 2024
@Vtec234
Copy link
Collaborator

Vtec234 commented Dec 20, 2024

Hi! That does look like something is wrong with your Node.js. However, if you are just using ProofWidgets4, you shouldn't need Node.js at all: see here. Can you paste your lakefile.toml or lakefile.lean?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
question Further information is requested
Projects
None yet
Development

No branches or pull requests

2 participants