Update dev-setup script to support Ubuntu 20.04 and 22.04 #1684

marsella · 2024-06-11T13:53:24Z

This adds Ubuntu support to the dev-setup script. Makes progress toward, but does not complete, #1673.

Adds some very minimalist Dockerfiles to use for testing
Adds ubuntu support throughout the script
Moves script + docker stuff into a dev/ directory for containment

Due to the last item, the diff on here is unhelpful. Consider reviewing without the first commit, which will better show you the changes in the script.

Some questions for reviewers:

In order to test the Ubuntu versions correctly from Apple hardware, you sometimes need to specify the platform to use when building and running the docker container (I had to do it the first time I built the container, but it seemed like subsequent builds remembered). Where should this documentation live?

$ docker build -t cryptol-ubuntu-22 --platform linux/amd64 -f ubuntu22.04.Dockerfile

To keep things simple, I'm using the z3 version packaged in what4-solvers. The readme for that repo suggests using the latest version of z3 (4.13.0) but provides a much older version (4.8.something). Should I download the latest version via other means, instead?

- clarifies errors that should be unreachable - reduces duplication with a function to check version

dev/dev_setup.sh

marsella · 2024-06-11T14:14:34Z

dev/ubuntu20.04.Dockerfile

+RUN ["apt-get", "install", "-y", "git"]
+RUN ["git", "clone", "https://github.com/GaloisInc/cryptol.git"]
+
+COPY dev_setup.sh ./cryptol/


todo: oops, this is a testing artifact. I will update this to run the setup script in the repo instead. Ditto below.

Fixed this. It technically won't work for anyone testing before this is merged because the dev setup script isn't in main; you can test locally by adding "-b", "add-ubuntu-dev-setup" to the clone line.

mccleeary-galois · 2024-06-11T16:07:10Z

This adds Ubuntu support to the dev-setup script. Makes progress toward, but does not complete, #1673.

Adds some very minimalist Dockerfiles to use for testing

Adds ubuntu support throughout the script

Moves script + docker stuff into a dev/ directory for containment

Due to the last item, the diff on here is unhelpful. Consider reviewing without the first commit, which will better show you the changes in the script.

Some questions for reviewers:

In order to test the Ubuntu versions correctly from Apple hardware, you sometimes need to specify the platform to use when building and running the docker container (I had to do it the first time I built the container, but it seemed like subsequent builds remembered). Where should this documentation live?
$ docker build -t cryptol-ubuntu-22 --platform linux/amd64 -f ubuntu22.04.Dockerfile
To keep things simple, I'm using the z3 version packaged in what4-solvers. The readme for that repo suggests using the latest version of z3 (4.13.0) but provides a much older version (4.8.something). Should I download the latest version via other means, instead?

We will want this type of documentation in the future README refactor in the dev setup part.

kquick · 2024-06-11T18:31:55Z

dev/dev_setup.sh

+install_zlib
+install_solvers
+put_brew_in_path
+set_ubuntu_language_encoding


I appreciate the way this structure summarizes the set of operations being performed. It is a good "self-documenting" summary of what the code is doing for both the user of this script or someone working in an environment this script doesn't support and who wants to know what it does. To support both of these, I'd recommend adding a reference to this portion in the preface comments; for example, add a "# Main operations" comment just above line 297 and then finish the paragraph in lines 10-13 with "For a list of the setup operations performed by this script, see the "Main Operations" section below (near the end of this file)."

This is nice, I added it.

kquick · 2024-06-11T18:36:45Z

dev/dev_setup.sh

+install_gmp
+install_zlib
+install_solvers
+put_brew_in_path


At first I was confused, thinking "Shouldn't this be the first operation? Most of the subsequent operations use brew (when on a Mac) so it seems like the brew path setup should precede them." but then I looked at the details and see this adds brew to the user's path in the env setup script.

I'm curious as to why that is done: if this script is responsible for setting up the user's dev environment by installing all the needed things, why would the user need access to brew?

Also, why isn't this setup needed for the PATH while the script operates? It seems like the script is already assuming brew is in the PATH?

Oh, this is just confusingly named. This puts the install directories that brew uses by default into the path. We do assume that you already have brew installed / accessible when you call the script (I added a note re: this to the top of the file). This makes sure that, if the script had to install any packages via brew, they'll be available in your path.

Maybe add_brew_prefix_to_path? or put_brew_packages_in_path.

Renaming would probably help. Whatever you prefer, although the latter proposed name sounds the most descriptive to me.

kquick · 2024-06-11T18:51:52Z

dev/dev_setup.sh

+install_zlib
+install_solvers
+put_brew_in_path
+set_ubuntu_language_encoding


This should probably be moved to the Dockerfile and we shouldn't be overriding the local user's locale settings.

Maybe it's worth warning the user if LANG or LC_x doesn't (case-insensitively?) contain "UTF-8" for their local environment, but other than that I think we shouldn't mess with the user's environment like this and just move it to the Dockerfile where we know it needs to be set to support UTF-8.

Also, the conventional wisdom is that you shouldn't set LC_ALL: it's intended as something the user can manually set as an override for all of the other LC_x settings. Maybe we decide we're OK with that for the constrained Docker environment, but there's probably a more direct LC_x setting (or just set all except LC_ALL) that is still effective.

I agree we should be careful with this, however another use case for this is to quickly set up VMs. Perhaps a warning + option to set language encoding? We can start handling optional flags for some things like this as well, but ideally we would have a 1 line of code (with possible flags) for setting up a VM as well.

Thanks, I did not know this wisdom! I played around a bit and it seems like just setting LANG is enough to get the tests to pass. I'll modify this section to check and print a warning, and to add the export LANG... line as a comment in the generated var file. That way someone knows there's a problem, can easily uncomment the line if they don't care about changing their settings, but the default behavior lets them decide how to solve the problem.

I'll also update the dockerfile to set these.

sauclovian-g

generally LGTM

dev/dev_setup.sh

dev/ubuntu22.04.Dockerfile

weaversa · 2024-06-13T13:35:57Z

dev/ubuntu20.04.Dockerfile

+RUN ["apt-get", "-y", "upgrade"]
+RUN ["apt-get", "-y", "update"]
+RUN ["apt-get", "install", "-y", "git"]


Each RUN statement creates a layer in the Docker image. This can artificially increase the size of images. Official Docker best practice can be found here: https://docs.docker.com/build/building/best-practices/#run

After re-reading the best practice, I see there are also caching issues that make chaining apt-get RUN commands necessary. Wow.

Thanks for flagging this, I've seen the pattern of chaining apt-get commands before but didn't realize why.

For what it's worth, I'm not going to do a full apt-get clean here because we do install additional packages in the setup script; if maximally optimizing for size of the image is important, we could install all those packages here and then delete the rest of the apt-get cache, but it seems like it doesn't save a ton of space so I'm going to save that for later.

- handle non-debian linux platforms correctly - reduce automatic destruction of user language settings - improve documentation - fix dockerfiles to actually run the script

marsella · 2024-06-13T18:47:12Z

Thanks, all! I think I've addressed all feedback. I'm iterating on making sure that the sourcing step of the dockerfiles works correctly, for some reason it's not as straightforward as I expected. But other comments are hopefully now resolve-able.

We will want this type of documentation in the future README refactor in the dev setup part.

Cool. I added a note to the Dockerfiles for now so it doesn't get lost / forgotten.

kquick · 2024-06-13T19:07:17Z

dev/dev_setup.sh

+USED_BREW=false
+
+# Returns a string indicating the platform (from the set above), or empty if
+# a supported platform is not detected.


I would suggest returning a non-blank value here (e.g. maybe "unknown-platform" or something like that). The reason is that blank results can trip up shell scripts unless special care is taken to guard against their presence (e.g. case $blank_value in ... becomes case in ... and if [ ubuntu -eq $BLANK ] ... becomes if [ ubuntu -eq ] ...). I don't know that to be the case herein, it's just a preventative measure.

When we call this function we check right away if it's blank and exit if so, so it shouldn't cause issues anywhere else.

- change dockerfiles to hardcode environment variables instead of trying to source them from the script - Fix a typo in setting LANG

sauclovian-g · 2024-06-14T03:34:16Z

dev/dev_setup.sh

+                notice "    You may need to set them to UTF-8."
+                notice "    Uncomment the LANG var in $VAR_FILE before sourcing to do so"
+                echo "# uncomment the following lines to fix decoding errors e.g. hGetContents" >> $VAR_FILE
+                echo "# export LANG=C.UTF-8" >> $VAR_FILE


I remember some time back I filed a bug report with I think Debian that there was no C.UTF-8 locale and they rejected it. That was years ago and they have probably grown up since, but maybe not. (No need to do anything different here for now, but we might end up needing to revisit it sometime later. JFYI)

sauclovian-g · 2024-06-14T03:36:54Z

dev/dev_setup.sh

-            echo "export LANG=C.UTF-8" >> $VAR_FILE
-            echo "export LC_ALL=C.UTF-8" >> $VAR_FILE;;
-        *) ;;
+            if $LANG!= *"UTF-8"* || $LANG != *"utf-8"*; then


I don't think this conditional is going to work. Try

case x"$LANG" in *UTF-8*|*utf-8*) ;; *) notice ... ;;

(the x makes it not croak if the variable isn't set)

dev/ubuntu20.04.Dockerfile

mccleeary-galois

LGTM we can always iterate in the future if needed.

marsella added 5 commits June 11, 2024 09:38

dev-setup: move script to dev/ dir #1673

8df304d

dev-setup: add minimal docker for ubuntu 20 #1673

cb9b2b2

dev-setup: add support for ubuntu 20.04 #1673

73a6e68

dev-setup: add support for ubuntu-22.04 #1673

918335b

dev-setup: prettify script #1673

1952c8b

- clarifies errors that should be unreachable - reduces duplication with a function to check version

marsella temporarily deployed to github-pages June 11, 2024 13:53 — with GitHub Actions Inactive

marsella commented Jun 11, 2024

View reviewed changes

dev/dev_setup.sh Show resolved Hide resolved

dev/dev_setup.sh Show resolved Hide resolved

dev/dev_setup.sh Show resolved Hide resolved

marsella commented Jun 11, 2024

View reviewed changes

mccleeary-galois self-requested a review June 11, 2024 15:26

kquick reviewed Jun 11, 2024

View reviewed changes

sauclovian-g approved these changes Jun 13, 2024

View reviewed changes

dev/dev_setup.sh Show resolved Hide resolved

dev/ubuntu22.04.Dockerfile Outdated Show resolved Hide resolved

weaversa reviewed Jun 13, 2024

View reviewed changes

dev-setup: small script improvements #1673

05392cf

- handle non-debian linux platforms correctly - reduce automatic destruction of user language settings - improve documentation - fix dockerfiles to actually run the script

marsella temporarily deployed to github-pages June 13, 2024 18:10 — with GitHub Actions Inactive

kquick reviewed Jun 13, 2024

View reviewed changes

dev-script: fix env variable handling #1673

36a6f57

- change dockerfiles to hardcode environment variables instead of trying to source them from the script - Fix a typo in setting LANG

marsella temporarily deployed to github-pages June 13, 2024 21:33 — with GitHub Actions Inactive

sauclovian-g reviewed Jun 14, 2024

View reviewed changes

dev/ubuntu20.04.Dockerfile Outdated Show resolved Hide resolved

mccleeary-galois approved these changes Jun 17, 2024

View reviewed changes

marsella merged commit 0ab12fa into master Jun 18, 2024
45 checks passed

marsella deleted the add-ubuntu-dev-setup branch June 18, 2024 12:01

Update dev-setup script to support Ubuntu 20.04 and 22.04 #1684

Update dev-setup script to support Ubuntu 20.04 and 22.04 #1684

Uh oh!

Conversation

marsella commented Jun 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mccleeary-galois commented Jun 11, 2024

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sauclovian-g left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

marsella commented Jun 13, 2024

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mccleeary-galois left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

marsella commented Jun 11, 2024 •

edited

Loading