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

uncaught compile error #200

Open
StevenClontz opened this issue Nov 30, 2024 · 3 comments
Open

uncaught compile error #200

StevenClontz opened this issue Nov 30, 2024 · 3 comments

Comments

@StevenClontz
Copy link
Member

I believe https://github.com/pi-base/data/tree/82a8e40903b87c395d5ec4acb75bea07abfe69dd has an error (asserting that the empty space is strongly Choquet), but for some reason it wasn't caught during the compile action...

@yhx-12243
Copy link
Contributor

I remember that, one thing worth noticed is that, in current repository, it can't even do a successful build at all in my local:

unsuccessful build

For example: https://github.com/pi-base/data/blob/main/spaces/S000171/properties/P000018.md?plain=1 have an empty description, so I comment it out months ago and forget it. But in the official online version it keeps running.

@yhx-12243
Copy link
Contributor

The things more outrageous was that, backend has no logic to deduce contradiction:

type CheckResult =
| { kind: 'bundle'; bundle: Bundle }
| {
kind: 'contradiction'
contradiction: { theorems: unknown[]; properties: unknown[] }
}
function check(bundle: Bundle, _: unknown): CheckResult {
return { kind: 'bundle', bundle }
}

Only frontend has and it didn't report to user:

if (result.kind === 'contradiction') {
store.update(s => ({ ...s, contradiction: result.contradiction }))
halt()
return
}

yhx-12243 added a commit to yhx-12243/pi-base-web that referenced this issue Dec 5, 2024
@StevenClontz
Copy link
Member Author

@jamesdabbs should have some time to review your PR in the coming weeks.

FWIW the backend used to check for errors as compile time, but maybe this was accidentally looked over when we transitioned from https://github.com/pi-base/compile to https://github.com/pi-base/web

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

No branches or pull requests

2 participants