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

Issue checking file #48

Closed
thomas-lamiaux opened this issue Sep 20, 2024 · 2 comments · Fixed by #65
Closed

Issue checking file #48

thomas-lamiaux opened this issue Sep 20, 2024 · 2 comments · Fixed by #65
Labels
bug feature Something isn't working with the feature Repository

Comments

@thomas-lamiaux
Copy link
Collaborator

There seem to be an issue with the docker image checking files which may be a bit too old due to web interface as as you can see it bug on a the type scope

   (nat + bool)%type
       : Set
  File "./SearchTutorial.v", line 191, characters 0-19:
  Error: Error: Scope type is not declared.

https://github.com/coq/platform-docs/actions/runs/10952451667/job/30411152058?pr=9#step:4:4624

@thomas-lamiaux
Copy link
Collaborator Author

coq/platform-docs-admins I suggest switching docker to 8.19 as it is the platform version so that it always work with the current version when downloaded, even if the web version bugs at the moment

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 21, 2024

I suggest switching docker to 8.19

OK to me.

Note that you forgot a @ to properly mention the team.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug feature Something isn't working with the feature Repository
Projects
Development

Successfully merging a pull request may close this issue.

2 participants