Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .claude/CLAUDE.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ To run a specific test suite, set `LEAN4_TEST_FOLDER` to one of: `bootstrap`, `i

## Architecture

This is a **Lerna monorepo** with npm workspaces containing five packages:
This is an **npm-workspaces monorepo** (with Nx as the task runner) containing five packages:

### Packages

Expand Down
1 change: 1 addition & 0 deletions .eslintrc.js
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ https://github.com/typescript-eslint/tslint-to-eslint-config/blob/master/docs/FA
Happy linting! 💖
*/
module.exports = {
root: true,
env: {
es6: true,
node: true,
Expand Down
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ build/

## Output
node_modules/
.nx/
*.tsbuildinfo
*.vsix
doit.cmd
Expand Down
7 changes: 4 additions & 3 deletions lean4-infoview/src/infoview/info.tsx
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
import * as React from 'react'
import fastIsEqual from 'react-fast-compare'
import type { Location } from 'vscode-languageserver-protocol'

import {
Expand Down Expand Up @@ -482,14 +483,14 @@ function InfoAux(props: InfoProps) {
React.useEffect(() => {
// Note: the curly braces are important. https://medium.com/geekculture/react-uncaught-typeerror-destroy-is-not-a-function-192738a6e79b
setLspDiagsHere(diags0 => {
const diagPred = (d: LeanDiagnostic) =>
const isHere = (d: LeanDiagnostic) =>
RangeHelpers.contains(
d.fullRange || d.range,
{ line: pos.line, character: pos.character },
config.allErrorsOnLine,
)
const newDiags = (lspDiags.get(pos.uri) || []).filter(diagPred)
if (newDiags.length === diags0.length && newDiags.every((d, i) => d === diags0[i])) return diags0
const newDiags = (lspDiags.get(pos.uri) || []).filter(isHere)
if (newDiags.length === diags0.length && newDiags.every((d, i) => fastIsEqual(d, diags0[i]))) return diags0
return newDiags
})
}, [lspDiags, pos.uri, pos.line, pos.character, config.allErrorsOnLine])
Expand Down
4 changes: 0 additions & 4 deletions lerna.json

This file was deleted.

13 changes: 13 additions & 0 deletions nx.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
{
"$schema": "./node_modules/nx/schemas/nx-schema.json",
"targetDefaults": {
"build": {
"dependsOn": ["^build"]
},
"build:dev": {
"dependsOn": ["^build:dev"]
}
},
"parallel": 5,
"analytics": false
}
Loading
Loading