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.

Sign up for GitHub

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

Jump to bottom

chore: add .gitpod.yml and .docker/gitpod/Dockerfile #732

Merged
merged 2 commits into from
Apr 18, 2024
Merged

chore: add .gitpod.yml and .docker/gitpod/Dockerfile #732

merged 2 commits into from
Apr 18, 2024

Conversation

austinletson
Copy link
Contributor

Add docker files and .gitpod.yml to enable use of Gitpod with std4. Both of these are copied from mathlib with modifications for std4

I have opened std4 in Gitpod and tested,

  • building std4
  • running tests with make
  • building and view docs

related to #565

@austinletson austinletson changed the title feat: add .gitpod.yml and .docker/gitpod/Dockerfile chore: add .gitpod.yml and .docker/gitpod/Dockerfile Apr 12, 2024
@austinletson
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Apr 12, 2024
kim-em
kim-em reviewed Apr 17, 2024
View reviewed changes
.docker/gitpod/Dockerfile Outdated

USER root

RUN apt-get update && apt-get install sudo git curl git bash-completion python3 python3-requests gcc make -y && apt-get clean
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think we should need any python3 anymore. (Ideally we'd also remove this on the mathlib side).

There's also a repeated git here.

Could you test without?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have removed git and python3 and ran everything again successfully.

I didn't remove python3-requests. We still need that right? If you remove it you can't run python3 -m http.server to expose the documentation.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess --- I've never done that. I guess it doesn't hurt too much having python bundled in.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Alright, my thinking was that all the commands in the README.md should work out of the box.

I just launched Gitpod successfully from https://github.com/leanprover/std4 and built std4. Thanks!

@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Apr 17, 2024
@austinletson
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels Apr 17, 2024
@kim-em kim-em merged commit 62c35ea into leanprover-community:main Apr 18, 2024
1 check passed
@kim-em kim-em mentioned this pull request Aug 14, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees

@kim-em kim-em

Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@austinletson @kim-em