You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The current solution to prebuild the gitpod docker image using github
actions does not work nicely, since prebuilds triggered shortly after a
new release still use the old gitpod image (and it may take up to a few
days until the new image is available). This is especially notable for
the `develop` branch, which is the default entry point if you want to
start a new branch on gitpod.
In this ticket, we migrate the gitpod config to use the conda
environment, which is now generally stable enough for serious
development (e.g. almost all tests pass). As a positive side effect, the
gitpod config simplifies and startup times are considerably reduced.
URL: https://trac.sagemath.org/33739
Reported by: gh-tobiasdiez
Ticket author(s): Tobias Diez
Reviewer(s): Matthias Koeppe
## In order to push to trac, generate a new key with `ssh-keygen -f tempkey` and save the private key to gitpod `gp env PRIVATE_SSH_KEY="$(<tempkey)"` (or by following https://www.gitpod.io/docs/environment-variables#using-the-account-settings)
41
32
## then follow https://doc.sagemath.org/html/en/developer/trac.html#linking-your-public-key-to-your-trac-account to register the public key with trac.
@@ -47,7 +38,7 @@ tasks:
47
38
echo $PRIVATE_SSH_KEY | sed 's/\(-----\(BEGIN\|END\) OPENSSH PRIVATE KEY-----\)/\n\1\n/g' > ~/.ssh/id_rsa
mkdir -p logs && echo '### .gitpod.yml Setup.before: Prebuild init script has been run. Running "make" again in case the build had timed out.' >> logs/install.log
69
-
# The init script has already populated the SAGE_LOCAL,
70
-
# but only /workspace is preserved; and the $HOME/sage-local may contain a resurrected
71
-
# copy of sage-local. Replace it again by a symlink.
72
-
rm -Rf $HOME/sage-local
73
-
ln -sf $(pwd)/local $HOME/sage-local
74
-
# Now run make. No timeout here.
75
-
MAKE='make -j24' make build V=0
76
-
else
77
-
# Prebuild init script has not been run
78
-
# Only /workspace is preserved during build.
79
-
# If the Docker image contains a built SAGE_LOCAL, use it to populate the SAGE_LOCAL in the workspace.
80
-
if [ -d $HOME/sage-local ]; then
81
-
mv $HOME/sage-local local
82
-
fi
83
-
rm -Rf $HOME/sage-local
84
-
ln -sf $(pwd)/local $HOME/sage-local
85
-
# Save the logs of the source tree used by the Docker build
86
-
if [ -d $HOME/sage/logs ]; then
87
-
mv $HOME/sage/logs logs
88
-
fi
89
-
fi
90
-
# Remove the source tree used by the Docker build and replace it by a symlink
0 commit comments