Make docker images from tox/GitHub CI workflow, regular Sage Docker images, gitpod, CoCalc interoperable

[mkoeppe]

1. Adjust directory names to something that works for both cases ...

   • docker/Dockerfile currently has:
     • SAGE_ROOT=/home/sage/sage
     • SAGE_LOCAL=$SAGE_ROOT/local
   • Docker images built with tox/GH Actions (including Gitpod) and also computop/sage have:
     • SAGE_ROOT=/sage
     • SAGE_LOCAL=/sage/local
   • After this ticket:
     • SAGE_ROOT=/sage
     • SAGE_LOCAL=/opt/sage
   • CoCalc Docker image has:
     • SAGE_ROOT=/usr/local/sage
     • SAGE_LOCAL=/usr/local/sage/local

2. Script package _develop; improve installation instructions in the manual #33851: Define a script package representing "useful stuff to have on a Docker image"

3. Replace all apt-get in docker/Dockerfile by using a Docker image built using build/bin/write-dockerfile as the base image.

4. By default, docker/Dockerfile would use configure --without-system-... a lot so that CI is done against "the reference distribution"

5. Move build/bin/write-dockerfile.sh into docker/

6. Add a mechanism (environment variable) to tox -e docker... to copy SAGE_LOCAL from a given Docker image.

CC: @kliem @dimpase @embray @saraedum @slel @fchapoton @tobiasdiez @williamstein @culler @NathanDunfield

Component: docker

Keywords: ci, ContinuousIntegration, sd109

Issue created by migration from https://trac.sagemath.org/ticket/29536

[mkoeppe]

Description changed:

--- 
+++ 
@@ -1,3 +1,7 @@
 ... by adjusting directory names to something that works for both cases ...
 
+`docker/Dockerfile`:
+- `SAGE_ROOT=/home/sage/sage`
+- `SAGE_LOCAL=$SAGE_ROOT/local`
 
+

[dimpase]

comment:2

by the way, we don't seem to have in docs an explanation regarding file shared between docker images and regular file system of the host system.

[mkoeppe]

Changed keywords from ci, ContinuousIntegration to ci, ContinuousIntegration, sd109

[mkoeppe]

Description changed:

--- 
+++ 
@@ -1,7 +1,12 @@
-... by adjusting directory names to something that works for both cases ...
+1. adjust directory names to something that works for both cases ...
 
-`docker/Dockerfile`:
-- `SAGE_ROOT=/home/sage/sage`
-- `SAGE_LOCAL=$SAGE_ROOT/local`
+   `docker/Dockerfile`:
+   - `SAGE_ROOT=/home/sage/sage`
+   - `SAGE_LOCAL=$SAGE_ROOT/local`
 
+2. Define a script package representing "useful stuff to have on a Docker image" (more than the `_recommended` package from #29557)
 
+3. Replace all `apt-get` in `docker/Dockerfile` by using a Docker image built using `build/bin/write-dockerfile` as the base image.
+
+4. By default, `docker/Dockerfile` would use `configure --without-system-...` a lot so that CI is done against "the reference distribution"
+

[embray]

comment:5

I'm confused--should this say "GitHub" in the title or "GitLab"? I don't know of any GitHub CI docker images.

[dimpase]

comment:6

Replying to @embray:

I'm confused--should this say "GitHub" in the title or "GitLab"? I don't know of any GitHub CI docker images.

please see
https://doc.sagemath.org/html/en/developer/index.html#testing-on-multiple-platforms

we now have a builder of docker images for multiple platforms, configurable, and by default hosted on github.

[mkoeppe]

Description changed:

--- 
+++ 
@@ -1,8 +1,8 @@
 1. adjust directory names to something that works for both cases ...
 
-   `docker/Dockerfile`:
-   - `SAGE_ROOT=/home/sage/sage`
-   - `SAGE_LOCAL=$SAGE_ROOT/local`
+   `docker/Dockerfile` currently has:
+    - `SAGE_ROOT=/home/sage/sage`
+    - `SAGE_LOCAL=$SAGE_ROOT/local`
 
 2. Define a script package representing "useful stuff to have on a Docker image" (more than the `_recommended` package from #29557)
 

[mkoeppe]

Description changed:

--- 
+++ 
@@ -10,3 +10,7 @@
 
 4. By default, `docker/Dockerfile` would use `configure --without-system-...` a lot so that CI is done against "the reference distribution"
 
+
+5. Move `build/bin/write-dockerfile` into `docker/`
+
+

[mkoeppe]

Dependencies: #30960

[mkoeppe]

comment:14

Sage development has entered the release candidate phase for 9.3. Setting a new milestone for this ticket based on a cursory review of ticket status, priority, and last modification date.

[mkoeppe]

Description changed:

--- 
+++ 
@@ -13,4 +13,6 @@
 
 5. Move `build/bin/write-dockerfile` into `docker/`
 
+6. Add a mechanism (environment variable) to `tox -e docker...` to copy SAGE_LOCAL from a given Docker image.
 
+

[dimpase]

comment:17

Given that GitLab Docker build is broken for ages, can we arrange for GitHub-built docker images to be pushed to the main Docker repo,
or at least create some sort of advertised Docker repo on GitHub?

[mkoeppe]

Description changed:

--- 
+++ 
@@ -16,3 +16,5 @@
 6. Add a mechanism (environment variable) to `tox -e docker...` to copy SAGE_LOCAL from a given Docker image.
 
 
+
+Gitpod - see #32749

[mkoeppe]

comment:22

Bikeshedding time! Let's pick SAGE_ROOT, SAGE_LOCAL. My proposal is in the ticket description.

(The only important constraint for me is: Don't nest SAGE_LOCAL within SAGE_ROOT - for flexibility such as bind-mounting a new version of the source tree over SAGE_ROOT without hiding SAGE_LOCAL.)

[mkoeppe]

Description changed:

--- 
+++ 
@@ -1,20 +1,24 @@
-1. adjust directory names to something that works for both cases ...
-
-   `docker/Dockerfile` currently has:
-    - `SAGE_ROOT=/home/sage/sage`
-    - `SAGE_LOCAL=$SAGE_ROOT/local`
+1. Adjust directory names to something that works for both cases ...
+   - `docker/Dockerfile` currently has:
+      - `SAGE_ROOT=/home/sage/sage`
+      - `SAGE_LOCAL=$SAGE_ROOT/local`
+   - Docker images built with tox/GH Actions (including Gitpod) have:
+      - `SAGE_ROOT=/sage`
+      - `SAGE_LOCAL=/sage/local`
+   - **After this ticket:**
+      - `SAGE_ROOT=/sage`
+      - `SAGE_LOCAL=/opt/sage`
 
 2. Define a script package representing "useful stuff to have on a Docker image" (more than the `_recommended` package from #29557)
+   - perhaps call it `_devtools`? 
 
 3. Replace all `apt-get` in `docker/Dockerfile` by using a Docker image built using `build/bin/write-dockerfile` as the base image.
 
 4. By default, `docker/Dockerfile` would use `configure --without-system-...` a lot so that CI is done against "the reference distribution"
 
 
-5. Move `build/bin/write-dockerfile` into `docker/`
+5. Move `build/bin/write-dockerfile.sh` into `docker/`
 
 6. Add a mechanism (environment variable) to `tox -e docker...` to copy SAGE_LOCAL from a given Docker image.
 
 
-
-Gitpod - see #32749