Skip to content

Conversation

@pgiarrusso-sl
Copy link
Contributor

No description provided.

@github-actions
Copy link

github-actions bot commented Nov 3, 2025

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19040274869

Relative Master MR Change Filename
+0.00% 116596.1 116596.1 +0.0 total
-0.00% 22020.0 22019.8 -0.1 ├ translation units
+0.00% 94576.2 94576.2 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 116596.1 116596.1 +0.0 total
-0.00% 22020.0 22019.8 -0.1 ├ translation units
+0.00% 94576.2 94576.2 +0.0 └ proofs and tests

@rlepigre-skylabs-ai
Copy link
Contributor

For reference, here is what we used to have before:

{
	"name": "FM Default",
	"image": "ghcr.io/skylabsai/skylabs-fm:fm-default",

	"customizations": {
		"vscode": {
			"settings": {
				"vscoq.path": "/workspaces/skylabs-fm/_build/install/default/bin/vscoqtop"
			},
			"extensions": [
				"maximedenes.vscoq",
				"ocamllabs.ocaml-platform"
			]
		}
	},
	"mounts": [
		"source=${localEnv:HOME}/.cache/dune,target=/home/coq/.cache/dune,type=bind,consistency=cached"
	]
}

Copy link
Contributor

@rlepigre-skylabs-ai rlepigre-skylabs-ai left a comment

Choose a reason for hiding this comment

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

I think it would make sense to at least change the name.

Maybe we should also bring in the cache mounting we had in the config I posted above, and the OCaml extension?

We were also using a different vsrocq extension it seems?

@pgiarrusso-sl
Copy link
Contributor Author

What I sent is simplified from https://github.com/SkylabsAI/fm-ci/blob/main/devcontainer/devcontainer.json, documented in
https://github.com/SkylabsAI/fm-ci/blob/main/devcontainer/README.md.

  • "maximedenes.vscoq" got renamed to vsrocq, we can merge the other extensions — and drop versions from vsrocq
  • should we share the cache with the host? That seems iffy. It'll work, but I'd rather clear the devcontainer cache whenever the image changes.

@pgiarrusso-sl
Copy link
Contributor Author

pgiarrusso-sl commented Nov 3, 2025

ah, https://containers.dev/implementors/json_reference/#variables-in-devcontainerjson supports defaults! Then we can maybe have our cake and eat it too — at least if nested references work:

"source=${localEnv:DUNE_CACHE_DOCKER:${localEnv:HOME}/.cache/dune},target=/home/coq/.cache/dune,type=bind,consistency=cached"

EDIT: I can check devcontainers/spec#255.

@rlepigre-skylabs-ai
Copy link
Contributor

I only care that the cache used in the devcontainer is shared among different instances of the devcontainer.

I guess we could eventually allow people to locally mount the NFS cache? Though this might not be an improvement depending on the network.

@pgiarrusso-sl pgiarrusso-sl self-assigned this Nov 12, 2025
@github-actions
Copy link

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19303425469

Relative Master MR Change Filename
-0.00% 116925.3 116925.3 -0.0 total
-0.00% 22013.8 22013.9 -0.0 ├ translation units
+0.00% 94911.5 94911.5 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 116925.3 116925.3 -0.0 total
-0.00% 22013.8 22013.9 -0.0 ├ translation units
+0.00% 94911.5 94911.5 +0.0 └ proofs and tests

@github-actions
Copy link

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19305940636

Relative Master MR Change Filename
+0.00% 116925.3 116925.3 +0.0 total
+0.00% 22013.8 22013.8 +0.0 ├ translation units
+0.00% 94911.5 94911.5 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 116925.3 116925.3 +0.0 total
+0.00% 22013.8 22013.8 +0.0 ├ translation units
+0.00% 94911.5 94911.5 +0.0 └ proofs and tests

@pgiarrusso-sl
Copy link
Contributor Author

We discussed and tested this together, so merging.

@pgiarrusso-sl pgiarrusso-sl merged commit fc4a36c into main Nov 12, 2025
15 checks passed
@pgiarrusso-sl pgiarrusso-sl deleted the paolo/devcontainer branch November 12, 2025 18:29
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

Successfully merging this pull request may close these issues.

4 participants