Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Some little improvements #47

Merged
merged 1 commit into from
Feb 7, 2023

Conversation

guillep
Copy link
Contributor

@guillep guillep commented Feb 2, 2023

  • updated for Pharo 11
  • finding z3 in M1 installations
  • add a comment to bit vector class with an example

@guillep
Copy link
Contributor Author

guillep commented Feb 3, 2023

The full pharo build fails because of this error, that seems unrelated:

Run make -C pharo
  make -C pharo
  shell: C:\Program Files\PowerShell\7\pwsh.EXE -command ". '{0}'"
  env:
    PROJECT: MachineArithmetic
    Z3_DOWNLOAD_URL_WINDOWS: https://github.com/Z3Prover/z3/releases/download/z3-4.8.17/z3-4.8.17-x64-win.zip
make: Entering directory '/d/a/MachineArithmetic/MachineArithmetic/pharo'
GNUmakefile:3: GNUmakefile.local: No such file or directory
make: Leaving directory '/d/a/MachineArithmetic/MachineArithmetic/pharo'
Error: Process completed with exit code 1.

@guillep
Copy link
Contributor Author

guillep commented Feb 3, 2023

The other one seems to fail in ST/X because of my changes. But there are two of them:

  • self assert: a = b => self assert: a equals: b that was rewritten by a lint rule
  • a handle => a getHandle rewritten by an automatic deprecation

I'll undo those for now, but it raises the question:

  • is there a way to get the stack trace from the CI? :)
  • are those changes interesting/important? should I make another PR for them in isolation?

@shingarov
Copy link
Owner

This is definitely a very welcome PR.

A few nitpicks before this can be merged:

In 2d347, why are you proposing to duplicate SmalltalkImage>>isPharo in MachineArithmetic-FFI-Pharo? Or was this unintentional?

Removing MachineArithmetic/README.md in 0616c (breaking the "Bindings" link in Z3's main README) and re-adding it in 75ebc seems like unintended cross-commit noise, a bit of history-grooming would be good here.

0616c breaks Mac for everyone else because they are using Pharo 8 (and that's what the automatic scripts, such as the GNUmakefile, in this repo and numerous other Smalltalk-25 repos, are coded to use) and there is no FFIMacLibraryFinder in Pharo 8. Wait, how does this pass CI if this doesn't even compile?.. oh I see, CI never touches #macLibraryName (because we don't have a Mac task -- someone should add one). In any case I think the ldd-path problem this commit is addressing, should be considered a system-level issue. On my Intel Mac, the brew is in /usr/local/Cellar and so the Z3 lib is /usr/local/Cellar/z3/4.8.10/lib/libz3.dylib, and the ldd-interpreter is finding it just fine.

To expedite merging of this PR, I would recommend dropping 75ebc for now. What is and what isn't a good comment, is subject of controversy among the current contributors to Smalltalk-25, so no matter what you and I might come up with, we would be criticized either way. So I propose we simply steer clear of this for now.

Finally, I would reword the commit message in 2d347 to say something like "Remove deprecated sends of #handle". For commit messages (and other things) we follow the community guidelines in cases where major upstream projects (gem5, Eclipse, GDB) are in consensus; in this case in particular, those guidelines explicitly say "the first line of the commit message should be in imperative mood" and we want to be consistent with the rest of the open-source world.

So yeah, what I am proposing for this PR, is to keep only 2d347, get rid of the #isPharo hunk, and reword. We'll merge it like that, and whatever remains will go into a new PR.

@shingarov
Copy link
Owner

shingarov commented Feb 3, 2023

The full pharo build fails because of this error, that seems unrelated

That's for @janvrany .
Jan, can you please fix this? It was biting us during our last microhackathon, too.
What I am surprised by, is the passing CI report I am seeing.

@shingarov
Copy link
Owner

a handle => a getHandle rewritten by an automatic deprecation

I'll undo those for now

I don't get it. What remains of "Update for Pharo 11" then?

Perhaps we should have a quick call with @janvrany when he comes online?

@guillep
Copy link
Contributor Author

guillep commented Feb 3, 2023

I added SmalltalkImage>>isPharo because I got a DNU :)
Mea culpa, I couldn't find the method and I assumed it got lost ^^.
Maybe there is just something missing in the download instructions or I made a mistake?

I think that there is not much left in this PR finally :P.
But it's good to engage in the discussion, nothing is lost, it's just transformed.

So, to summarise:

  • I believe we can close this issue
  • We can make a short call if you want for the "update to Pharo11", but it's so small thing that maybe a mail suffices
  • I'll explore on my side why the isPharo method was not there and I'll come back!

@guillep
Copy link
Contributor Author

guillep commented Feb 3, 2023

BTW, I was super happy I made the example I needed work yesterday :)
What do you think would be a nice place to put more "user-oriented" documentation?
I can keep it on my side, that's not a problem, but maybe you would like to centralize it more around this repo.

@shingarov
Copy link
Owner

if you want for the "update to Pharo11", but it's so small thing

Well, we are pretty interested in getting off of the long-outdated Pharo 8. See, for example, Issue 24. So when you submit a PR which says "This make MA work on Pharo11", we are obviously excited.

@shingarov
Copy link
Owner

What do you think would be a nice place to put more "user-oriented" documentation?

The steep learning curve for Z3, for SMT in general, for MachineArithmetic which is not just an FFI for Z3 but on top of that contains a dependent type system, so there is the learning curve related to dependent types -- that's a very big and painful problem (and we haven't even gotten to the "interesting applications" of MachineArithmetic, such as PharoArchC or TinyRossa!), and what documentation is appropriate as "user-oriented", to me this seems like a huge open-ended question. Its discussion definitely doesn't fit in this PR thread; we can discuss separately.

@janvrany
Copy link
Collaborator

janvrany commented Feb 3, 2023

is there a way to get the stack trace from the CI? :)

Not right now. For St/X maybe I can archive JUnit .xml report.
On Pharo, I do now know how to force it to generate a report in addition to writing output
to stdout and correctly propagating status code. But yes, this would be nice to have.

That's for @janvrany .
Jan, can you please fix this? It was biting us during our last microhackathon, too.

Having a look right now.

Perhaps we should have a quick call with @janvrany when he comes online?

I'm in my office now, will be here until say 3:30pm UK time. Just ping in BA slack.

@janvrany
Copy link
Collaborator

janvrany commented Feb 3, 2023

Jan, can you please fix this? It was biting us during our last microhackathon, too.

Sigh, it seems to me MS changed something in Windows runner, this build
https://github.com/shingarov/MachineArithmetic/actions/runs/3505530777 2 months ago passes, this one from today does not https://github.com/shingarov/MachineArithmetic/actions/runs/4083841051. Both runs use the exact same commit.

@shingarov
Copy link
Owner

Sigh, it seems to me MS changed something in Windows runner

I don't get it. What does Windows have to do with GNUmakefile.local? At the microhackathon we were seeing it on Linux; and I believe @guillep is seeing it on Mac?

@janvrany
Copy link
Collaborator

janvrany commented Feb 3, 2023

I think I fixed Windows build problem:

https://github.com/shingarov/MachineArithmetic/actions/runs/4084147512

So, to summarise:

  • I believe we can close this issue
  • We can make a short call if you want for the "update to Pharo11", but it's so small thing that maybe a mail suffices
  • I'll explore on my side why the isPharo method was not there and I'll come back!

isPharo is defined in PreSmalltalks-Pharo which prerequsite of MA.

@janvrany
Copy link
Collaborator

janvrany commented Feb 3, 2023

Sigh, it seems to me MS changed something in Windows runner

I don't get it. What does Windows have to do with GNUmakefile.local? At the microhackathon we were seeing it on Linux; and I believe @guillep is seeing it on Mac?

The error @guillep was referring was from Windows CI runner.
The core of the problem is thatGNUmakefile.local is included early in GNUmakefile since it contains local customizations. However, the GNUmakefile also contained a rule to generate it with some comments so it is easy to see what you can customize.

So because of my ignorance, we ended up in situation when an attempt to include non-existent GNUmakefile.local invoked target GNUmakefile.local but in order to build it, you need to include it first so you have a enless loop in make.

Now, apparently some versions of GNU make are smart enough to detect this and ignore the inclusion - this is case of my and your case, it "worked" just it did not created the GNUmakefile.local - this was the issue we bumped into with Tinyrossa.

Some other version seems to fail with an error.

@shingarov
Copy link
Owner

@guillep Do you still want the deprecation fix merged?

@janvrany
Copy link
Collaborator

janvrany commented Feb 6, 2023

I'll explore on my side why the isPharo method was not there and I'll come back!

I just understood why it was missing. This is because it is in PreSmalltalks-Pharo which is not loaded as part of Z3Only group. I thought it'd be pulled in since Z3only loads PreSmalltalks and PreSmalltalks depends on PreSmalltalks-Pharo but apparently not. My fault - clearly I still do not know how to use Metacello. Will fix it soon.

Note however, that once I fix it, the thing will stop working on Pharo 11 - see my comment in #24

@guillep
Copy link
Contributor Author

guillep commented Feb 6, 2023

I saw all the comments, but that makes me wonder. Why is isPharo in the PreSmalltalks package?
If it stays like that, Z3 will depend on it, but clearly, it's not required for Z3 to work... Couldn't that method be moved somewhere else?

@shingarov
Copy link
Owner

Oh, PreSmalltalks is definitely required for Z3 to work.

@guillep
Copy link
Contributor Author

guillep commented Feb 7, 2023

Oh, PreSmalltalks is definitely required for Z3 to work.

Ok, maybe it was just not needed for my small examples

@guillep
Copy link
Contributor Author

guillep commented Feb 7, 2023

@guillep Do you still want the deprecation fix merged?

It's not clear to me if that break St/x compatibility or not. Can @janvrany confirm?

@janvrany
Copy link
Collaborator

janvrany commented Feb 7, 2023

Looking at the code, For core Z3 isPharo is needed only in tests to skip certain tests on non-pharo dialects.

Why is isPharo in the PreSmalltalks package?

It is not specific to Z3, this is used on multiple places in this codebases and other that depend on it ( ArchC and Tinyrossa for example).
I'd argue the best place for this method would be in Pharo itself but well, such proposal was rejected long ago. So we had to put it somewhere.

Can @janvrany confirm?

Looking a the code, yes, it should be okay to use getHandle instead of handle. However, it'd be great if you can rebase atop of current pure-z3 branch and (force) push to have CI to check it.

@shingarov
Copy link
Owner

Looking at the code, For core Z3 isPharo is needed only in tests to skip certain tests on non-pharo dialects.

That wasn't my point. My point is, right now we assume PreSmalltalks is always present in all configurations (and this is true about all repos), simply because the day has 24hrs. My understanding of why Guille had to pull in isPharo was exactly because one of the configurations broke for him without it. No-one has the energy to maintain that kind of differentiation, we've got MUCH bigger fish to fry -- so we simply assume PreSmalltalks is there.

However, it'd be great if you can rebase atop of current pure-z3 branch and (force) push to have CI to check it.

I still suggest what I had suggested before: reset the branch to only contain 2d347, get rid of isPharo, (so now only the getHandle change is in the PR), reword the message, rebase, and force-push. If CI then passes (likely), I'll merge the PR.

@guillep guillep force-pushed the improvements/bitvectors branch from 27ea77b to 2936134 Compare February 7, 2023 16:30
@guillep guillep force-pushed the improvements/bitvectors branch from 2936134 to 25ff5f6 Compare February 7, 2023 16:50
@janvrany
Copy link
Collaborator

janvrany commented Feb 7, 2023

Thanks @guillep ! I'll let @shingarov to press the merge button.

@shingarov shingarov merged commit 5f30551 into shingarov:pure-z3 Feb 7, 2023
@guillep guillep deleted the improvements/bitvectors branch February 7, 2023 17:01
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.

3 participants