Dune based build #83

kape1395 · 2023-05-31T06:57:54Z

Closes #82

This PR extends the dune-based build started at #81.
This version supports running the tests and creating a release.

The changes are non-invasive, so the previous build/test process remains working.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

damiendoligez

Looks good except for the change to ocaml_versions.py.

I confirm that the change to fpfile.ml fixes a bug.

.github/workflows/ocaml_versions.py

This reverts commit fc7a310. Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

E.g. `gh act --secret GITHUB_TOKEN=.. --reuse` Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

kape1395 · 2023-06-08T15:55:15Z

The PR is ready to be reviewed. In general, it adds:

Make the build process familiar to other projects (make ; make test; make install; make release).
The distribution file is just an archive that is enough to extract to use (no installation).
The test cases can be run without making a release and installing it. Use make -C test -f Makefile.dune fast or similar. The shell autocompletion to select a more detailed test case works this way.
Tlaps, if built with dune, uses dune sites to locate the backend provers and stdlib tla files. This makes taps easier to use, as no PATH updates are needed. As a side-effect, other projects can supply their files to these locations (sites); thus, a plugin system is in place to use, e.g., to add additional tla libraries.

There are some problems still, but I hope those are not blockers:

I found no simple way to run unit (kaputt-based, provided in the mlt files) tests without breaking the existing build. There are a few of them; maybe I could rewrite them using ppx_inline_test or similar?
The current dune install step breaks the symlinks and exec permissions. As a workaround, I fix them afterward with a post-install script. I will try to make a fix/PR to the dune project, but its acceptance will not be fast, I guess. Then we could remove that workaround with the post-install script.
There are now two parallel build systems. Would you agree to remove the old one and keep the dune based only?
I cannot test the scripts on operating systems other than Linux. I would like to have help or pointers with this.

damiendoligez

This will need some work to make it run on MacOS and Windows.

damiendoligez · 2023-06-13T14:12:50Z

deps/isabelle/Makefile

@@ -0,0 +1,55 @@
+ISABELLE_VSN:=Isabelle2011-1
+ISABELLE_TGZ:=$(ISABELLE_VSN)_bundle_x86-linux.tar.gz


This fails in MacOS, and most probably on Windows.

In MacOS, you have to download a .dmg file, which is not a .tar.gz, and use a different set of commands to extract files from it. IOW, the recipe for $(ISABELLE_DIR): $(ISABELLE_TGZ) will have to be completely different. Does dune give you access to the OS name, or will you need to make this a Makefile.in and tweak configure?

I have updated the makefile to consider different OS types. Isabelle still doesn't work.

On MacOS, I'm getting poly: Bad CPU type in executable, I guess the 32 bit support is missing. At least it was needed on Linux for Isabelle to work.

On Cygwin, the following DLLs/Versions are missing: cyggcc_s-1.dll, cyggmp-3.dll and I can't find them for installation in the Cygwin package repository. The old release script was adding cyggmp-3.dll to the Isabelle, but the DLL is not committed to the repo; thus, I guess it should fail as well.

damiendoligez · 2023-06-13T14:16:39Z

deps/z3/Makefile

@@ -0,0 +1,20 @@
+Z3_VERS=4.8.9
+Z3_URL_PREFIX=https://github.com/Z3Prover/z3/releases/download/z3-$(Z3_VERS)
+Z3_BASE_NAME=z3-${Z3_VERS}-x64-ubuntu-16.04


Like Isabelle, this is not going to work on MacOS and Windows.

I have updated the makefiles (for all backends: z3, ls4, zenon and isabelle). All work on MacOS and Cygwin except the Isabelle (comments above).

damiendoligez · 2023-06-13T14:18:42Z

dune-project

+  "Kaustuv Chaudhuri"
+  "Denis Cousineau"
+  "Damien Doligez"
+  "Leslie Lamport"
+  "Tomer Libal"
+  "Stephan Merz"
+  "Jean-Baptiste Tristan"
+  "Hernan Vanzetto")
+ (maintainers
+  "Kaustuv Chaudhuri"
+  "Denis Cousineau"
+  "Damien Doligez"
+  "Leslie Lamport"
+  "Tomer Libal"
+  "Stephan Merz"
+  "Jean-Baptiste Tristan"
+  "Hernan Vanzetto")


Note to myself: update these lists.

src/dune_site_mock/setup_paths.ml

damiendoligez · 2023-06-13T14:34:01Z

src/params.ml

+    let site_isa bs = Filename.concat (Filename.concat bs "Isabelle") "bin" in
+    let site_paths bs = [site_bin bs; site_isa bs] in
+    let path_elems = List.concat (List.map site_paths backends_site) in
+      sprintf "%s:%s" (String.concat ":" path_elems) (Sys.getenv "PATH")


This is a pretty big change: you're putting the extra path elements at the beginning of PATH rather than the end.

My motivation for this change is to have the backends defined more predictably. E.g., I have an existing installation of TLAPM, and its backends are on the path. It is easy to accidentally forget to set the path to the new location and invoke a new TLAPM with old backends.

Behavior may be more predictable if TLAPM always used the backends shipped with it. We could introduce options to override specific backends, e.g., --with-z3=/home/.../bin/z3 and similar? Of course, an alternative to use environment variables could also be supported, e.g., export TLAPM_Z3=/home/.../bin/z3.

Some setups probably exploit the current implementation to look for backends in the PATH variable to override the backends. If the above proposal doesn't look good, I can put these paths at the end. This will also require updating the tests to avoid accidental overrides.

Coming back to this, I now think you're right: we should make it hard to accidentally override the provided backends. So let's keep this change and we'll add an override mechanism later if needed.

src/params.ml

tlapm.opam

test/TOOLS/do_junit_tests

zenon/regression/examples/data/TLAPS.tla

Co-authored-by: Damien Doligez <damien.doligez@gmail.com> Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

kape1395 · 2023-06-30T08:33:29Z

@damiendoligez, could you rerun the pipeline? I hope I have resolved the problems with MacOS.

damiendoligez · 2023-09-12T12:47:16Z

@kape1395 I don't have any button on my GitHub interface to trigger the CI checks.

damiendoligez

I've reviewed all the files that changed since my last review and everything looks good.

kape1395 · 2023-09-12T12:53:48Z

I've reviewed all the files that changed since my last review and everything looks good.

The checks are now executed. Maybe I have mistakenly assumed it is manual.

kape1395 · 2023-09-30T17:20:15Z

@muenchnerkindl, @damiendoligez, maybe this PR can be merged already?

kape1395 · 2023-10-10T19:18:01Z

@ahelwer, this is the PR I have updated the CI scripts.
There is room for improvement, especially when a release policy is decided.

ahelwer · 2023-10-10T19:19:55Z

@kape1395 okay cool, is there any obstacle to merging the PR? As you said it would be nice to get it in so we don't have PRs piling up on top of PRs. Don't have to issue a release yet.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

ahelwer · 2023-10-23T15:01:35Z

Hurrah it's merged! @kape1395 do you think this is a good time to add a CI step to test the newly-built TLAPM against the tlaplus/examples repo, like we do for the tools here? https://github.com/tlaplus/tlaplus/blob/dd9f38f26c184014086c37bff8a056b4d51f4464/.github/workflows/pr.yml#L54-L83

kape1395 · 2023-10-24T09:26:25Z

@ahelwer, that's probably a good time from the build-script changes perspective, but now #55 was also merged to the main branch and introduced a bug. One of the tests fails; it sounds related to CHOOSE handling or theorem expansion. I hope to look at it deeper next weekend.

kape1395 · 2023-10-24T09:28:28Z

@ahelwer, I have updated the build/install instructions with this PR. Probably that can be useful for you: https://github.com/tlaplus/tlapm/blob/main/INSTALL.md

ahelwer · 2023-10-24T16:01:10Z

@kape1395 okay cool! Once the new bug is fixed do you think it will be worth cutting a pre-release so we can start consuming it in the tlaplus/examples CI to test that the nondeterministic install bug was fixed?

kape1395 · 2023-10-24T16:20:11Z

This question is not to me probably. What do you think about using the latest main all the time? This way some kind of continuous integration would be implemented.

lemmy · 2023-10-24T16:26:13Z

We used to have that and I'm very much in favor or adding it again. :-)

ahelwer · 2023-10-25T01:26:15Z

I'd say that depends how much effort is necessary to build TLAPM from a checkout of main. The tlaplus tools are pushed to a nightly build server every time a commit hits main, which is nice, and we pull that down in the tlaplus/examples CI. Does this repo do anything similar?

ahelwer · 2023-10-27T14:53:40Z

@kape1395 I'm working on some changes to the CI to upload main builds to the Inria server. Unfortunately when I run make release locally I get:

make release
rm -rf _build/tlaps-release-dir _build/tlaps-release-version
dune install --relocatable --prefix _build/tlaps-release-dir
make -C _build/tlaps-release-dir/lib/tlapm -f Makefile.post-install
make[1]: Entering directory '/home/ahelwer/src/tlaplus/tlapm/_build/tlaps-release-dir/lib/tlapm'
chmod +x backends/bin/*
make -C backends -f Isabelle.post-install
make[2]: Entering directory '/home/ahelwer/src/tlaplus/tlapm/_build/tlaps-release-dir/lib/tlapm/backends'
make[2]: *** No rule to make target '\n\t', needed by 'all'.  Stop.
make[2]: Leaving directory '/home/ahelwer/src/tlaplus/tlapm/_build/tlaps-release-dir/lib/tlapm/backends'
make[1]: *** [Makefile.post-install:3: all] Error 2
make[1]: Leaving directory '/home/ahelwer/src/tlaplus/tlapm/_build/tlaps-release-dir/lib/tlapm'
make: *** [Makefile:50: release] Error 2

Tracking this down, it's because my _build/tlaps-release-dir/lib/tlapm/backends/Isabelle.post-install file contains:

FILES=(large list of files)
all:\n\t chmod +x $(FILES)

The \n\t thing looks suspicious, is this some bug in how a name was generated?

In general I just need to find the filepath of the make release output (the tlapm installer) so I can upload it to the server. What would that be?

kape1395 · 2023-10-27T15:47:41Z

What OS are you using locally? That could be some incompatibility in the CLI tools.
That line is generated in deps/isabelle/Makefile by the line

echo "all:\n\t chmod +x \$$(FILES)" >> $@

I guess in your OS, echo requires some flags (e.g., -e) to process escaped symbols properly.

Can you try changing that line to

echo -e "all:\n\t chmod +x \$$(FILES)" >> $@

kape1395 · 2023-10-27T15:52:31Z

Nah, it fails on my machine with -e added. Maybe there is a mismatch with the make versions? In my case that's

$ make --version
GNU Make 4.3
Built for x86_64-pc-linux-gnu
Copyright (C) 1988-2020 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

ahelwer · 2023-10-28T20:43:48Z

Hi @kape1395 I can confirm adding the -e flag to echo fixed the issue for me. I had some test failures but according to test/tests.log that's because I didn't have time installed. Now they pass.

My version of make is 4.4.1. I'm running Arch linux.

Anyway it isn't so much important for me to be able to build things locally, unless you think that's a problem. I'm more interested in figuring out where things are output so I can use them in the CI. I need to know where the .bin installer file is built so I can both upload it and also use it to run tests against tlaplus/examples.

kape1395 · 2023-10-28T21:20:23Z

You can check the error in files e.g.

./_build/default/test/fast/basic/cvc3_false_test.tla.err
./_build/default/test/fast/basic/cvc3_false_test.tla.out

and correspondingly for other test case files.

Adding -e is probably not enough, as that makes the script non-portable. For example, it fails on my machine. I will experiment with that.

By the way, why do you need the bin installer? There is no installer anymore.
After running

make build install

you can run tlapm e.g. as opam exec -- tlapm.
Or that's not enough to run the tests?
In my case, the tlapm exec is installed then as ~/.opam/5.1.0/lib/tlapm, but I think using opam exec is probably more convenient.

kape1395 added 8 commits May 27, 2023 23:11

Dune: deps, isabelle.

9da90a5

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Dune: deps, zenon.

a2cccbc

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Trying to make dune install work for deps.

113b1bf

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

deps: z3 and ls4.

9eb565a

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

deps: translate utility.

0d5fa15

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

install emacs mode.

451b04e

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

install: library.

040a5c3

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Try ocaml 4.08.2 instead of 4.08.1.

fc7a310

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

damiendoligez reviewed Jun 1, 2023

View reviewed changes

.github/workflows/ocaml_versions.py Outdated Show resolved Hide resolved

Revert "Try ocaml 4.08.2 instead of 4.08.1."

7826dec

This reverts commit fc7a310. Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

kape1395 force-pushed the support-dune-build-deps branch from 8dd911f to 7826dec Compare June 1, 2023 17:46

kape1395 added 11 commits June 2, 2023 00:05

Use dune-site to locate backends (partial).

9fe5a8d

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Run tests with dune (except the mlt files).

5638f17

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Able to run the testcases selectively.

8bc06c3

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Fix the existing build.

2422f4e

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Fix a warning.

1892e10

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Use stdlib site for the library TLA files.

3c21d96

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

github actions are now passing when rinning them locally.

ca5e8fd

E.g. `gh act --secret GITHUB_TOKEN=.. --reuse` Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Restore execution permissions after dune install.

6f80041

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Attempt to make 'opam install .' work.

e14db51

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Make target to install opam deps.

4cd3140

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Cleanup.

e3128d6

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

kape1395 marked this pull request as ready for review June 8, 2023 15:55

kape1395 requested a review from damiendoligez June 8, 2023 15:55

damiendoligez reviewed Jun 13, 2023

View reviewed changes

Update src/params.ml

0eb54fb

Co-authored-by: Damien Doligez <damien.doligez@gmail.com> Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

kape1395 force-pushed the support-dune-build-deps branch from ab134a7 to 0eb54fb Compare June 14, 2023 20:17

kape1395 added 2 commits June 14, 2023 23:18

The old build system removed.

94e1392

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Split tlapm to a lib and exec, only execs support inline tests.

f69774a

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

kape1395 requested a review from damiendoligez June 23, 2023 22:42

kape1395 added 2 commits June 24, 2023 18:44

Run a short test during the release.

620b9dc

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Use an opam.template to customize the build step for opam.

41c36d1

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

kape1395 mentioned this pull request Aug 13, 2023

Nondeterministic tlapm install failure on ubuntu (building Pure failed) #88

Open

damiendoligez approved these changes Sep 12, 2023

View reviewed changes

This was referenced Sep 17, 2023

OCaml 5.1 #91

Merged

LSP support #90

Closed

kape1395 mentioned this pull request Oct 10, 2023

Language Server Protocol for TLAPM #93

Merged

kape1395 added 2 commits October 13, 2023 22:30

Build/install procedures updated.

2bd1f82

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

Merge remote-tracking branch 'origin/main' into support-dune-build-deps

8f5c5c8

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

kape1395 mentioned this pull request Oct 22, 2023

Branch updated_enabled_cdot on top of dune, ocaml-5 and lsp. #95

Closed

damiendoligez merged commit 87a4f4c into tlaplus:main Oct 23, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Dune based build #83

Dune based build #83

kape1395 commented May 31, 2023

damiendoligez left a comment

kape1395 commented Jun 8, 2023

damiendoligez left a comment

damiendoligez Jun 13, 2023

kape1395 Jun 18, 2023

damiendoligez Jun 13, 2023

kape1395 Jun 18, 2023 •

edited

Loading

damiendoligez Jun 13, 2023

damiendoligez Jun 13, 2023

kape1395 Jun 22, 2023

damiendoligez Sep 12, 2023

kape1395 commented Jun 30, 2023

damiendoligez commented Sep 12, 2023

damiendoligez left a comment

kape1395 commented Sep 12, 2023

kape1395 commented Sep 30, 2023 •

edited

Loading

kape1395 commented Oct 10, 2023

ahelwer commented Oct 10, 2023

ahelwer commented Oct 23, 2023

kape1395 commented Oct 24, 2023

kape1395 commented Oct 24, 2023

ahelwer commented Oct 24, 2023

kape1395 commented Oct 24, 2023

lemmy commented Oct 24, 2023

ahelwer commented Oct 25, 2023

ahelwer commented Oct 27, 2023 •

edited

Loading

kape1395 commented Oct 27, 2023

kape1395 commented Oct 27, 2023

ahelwer commented Oct 28, 2023 •

edited

Loading

kape1395 commented Oct 28, 2023

		@@ -0,0 +1,55 @@
		ISABELLE_VSN:=Isabelle2011-1
		ISABELLE_TGZ:=$(ISABELLE_VSN)_bundle_x86-linux.tar.gz

Dune based build #83

Dune based build #83

Conversation

kape1395 commented May 31, 2023

damiendoligez left a comment

Choose a reason for hiding this comment

kape1395 commented Jun 8, 2023

damiendoligez left a comment

Choose a reason for hiding this comment

damiendoligez Jun 13, 2023

Choose a reason for hiding this comment

kape1395 Jun 18, 2023

Choose a reason for hiding this comment

damiendoligez Jun 13, 2023

Choose a reason for hiding this comment

kape1395 Jun 18, 2023 • edited Loading

Choose a reason for hiding this comment

damiendoligez Jun 13, 2023

Choose a reason for hiding this comment

damiendoligez Jun 13, 2023

Choose a reason for hiding this comment

kape1395 Jun 22, 2023

Choose a reason for hiding this comment

damiendoligez Sep 12, 2023

Choose a reason for hiding this comment

kape1395 commented Jun 30, 2023

damiendoligez commented Sep 12, 2023

damiendoligez left a comment

Choose a reason for hiding this comment

kape1395 commented Sep 12, 2023

kape1395 commented Sep 30, 2023 • edited Loading

kape1395 commented Oct 10, 2023

ahelwer commented Oct 10, 2023

ahelwer commented Oct 23, 2023

kape1395 commented Oct 24, 2023

kape1395 commented Oct 24, 2023

ahelwer commented Oct 24, 2023

kape1395 commented Oct 24, 2023

lemmy commented Oct 24, 2023

ahelwer commented Oct 25, 2023

ahelwer commented Oct 27, 2023 • edited Loading

kape1395 commented Oct 27, 2023

kape1395 commented Oct 27, 2023

ahelwer commented Oct 28, 2023 • edited Loading

kape1395 commented Oct 28, 2023

kape1395 Jun 18, 2023 •

edited

Loading

kape1395 commented Sep 30, 2023 •

edited

Loading

ahelwer commented Oct 27, 2023 •

edited

Loading

ahelwer commented Oct 28, 2023 •

edited

Loading