Closed pfdietz closed 5 years ago
Yes, I am always starting from scratch (the contents of the original zip file) when building ACL2 and then certifying books.
The log file has no errors - attaching it here. make-certify-books.log
Thanks - I'll be running the short test from now on.
Any updates?
Not yet - I still need to run the shorter tests multiple times to ensure that the results I am getting are correct and consistent.
I will attempt to build CCL master and CCL with PLNs from clean slate on a separate server and do that tomorrow.
On a different machine with 48 cores and free CPU, (time nice make -j 8 certify-books-short) >& make-certify-books2.log
repeated on CCL master and CCL master with PLNs gives me:
PLNs | No PLNs |
---|---|
4m47.245s | 4m47.484s |
4m43.847s | 4m43.070s |
4m41.379s | 4m42.088s |
4m43.597s | 4m43.675s |
4m28.394s | 4m41.052s |
4m29.494s | 4m25.936s |
4m45.449s | 4m46.193s |
4m33.784s | |
4m31.353s | |
4m44.196s |
From these four test runs, I can infer two things:
time nice make -j 8 certify-books
and time nice make -j 8 certify-books-short
aren't really fit for performance-testing CCL due to their big variance.@xrme @MattKaufmann @pfdietz Should I keep on testing?
The certify-books-short
target for make
is a relatively tiny test. I'd be more comfortable seeing what happens with some of the more compute-intensive books.
If you send me instructions for how to install your patch, I'm willing to do 5-hour runs(make
target regression-everything
) both ways, to compare times. I have tools that can help isolate any slowdown to specific files, and I can then compare performance on any files that are significantly impacted, on a machine where I have found timings to be quite consistent.
OK - I will run certify-books
overnight and see how it goes.
The instructions are in the first post.
I have managed to run one more certify-books
with -j 8
.
No PLNs:
real 165m38.178s
user 969m40.911s
sys 22m37.426s
PLNs:
real 167m48.616s
user 966m42.127s
sys 22m38.072s
Another run of certify-books
with -j 16
.
No PLNs:
real 122m52.725s
user 1083m51.261s
sys 22m42.468s
PLNs:
real 122m6.260s
user 1078m21.304s
sys 22m36.764s
These results seriously vary a lot between individual runs. In the above case, there were two minutes of difference in favor of no-PLN solution, and here, package-local nicknames are 45 seconds faster.
Yesterday I did complete runs on the ACL2 books and got only
trivial (0.016%) slowdown with the PLN patch, using
make -j 8 regression-everything-fresh
.
;;; Before the patch:
129906.436u 1964.668s 5:06:04.88 718.0% 0+0k 4137872+8829696io 1319pf+0w
;;; After the patch:
130098.192u 1851.232s 5:05:35.85 719.6% 0+0k 3553280+8805824io 1106pf+0w
(/ (+ (* 60 306) 04.88)
(+ (* 60 305) 35.85))
1.001583237210165
Another ACL2 user also did testing yesteray, and found that his run actually went about 0.3% faster with the PLN patch.
So as far as we can tell, the effect of the PLN patch on ACL2 speed is in the noise, and we have no objection to inclusion of the patch in CCL. Assuming it's functionally correct, of course -- that other user ran the tests provided by @phoe and found that 4 of 15 failed. Maybe it was an installation problem.
@MattKaufmann Thanks for the verification!
The issues highlighted by @solswords are correctness issues - I have likely not re-run the tests after inserting the modified versions of compiler macros for intern
, make-package
, ...
I will fix these issues on my fork, make sure that the tests pass, and then ask you for re-verification on your machine to ensure that no slowdown whatsoever slips by.
The tests themselves were faulty: see https://github.com/Clozure/ccl/pull/188#issuecomment-464071806
I think things are starting to look pretty promising here.
Ayup! I did not get any response from @solswords so far. What should we do? Is anyone else able/willing to review https://github.com/phoe/package-local-nicknames-tests on CCL and other implementations and ensure that they test what they are supposed to do?
It's the code review phase, in which I cannot really do too much since I'm the author of the patch set. It's best if another pair(s) of eyes look at what I've done.
I would be able to rerun the tests tomorrow, but unfortunately probably not today. I'm satisfied if someone else can verify though.
On Mon, Feb 18, 2019, 12:57 AM Michał Herda <notifications@github.com wrote:
Ayup! I did not get any response from @solswords https://github.com/solswords so far. What should we do? Is anyone else able/willing to review https://github.com/phoe/package-local-nicknames-tests on CCL and other implementations and ensure that they test what they are supposed to do?
It's the code review phase, in which I cannot really do too much since I'm the author of the patch set. It's best if another pair(s) of eyes look at what I've done.
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/Clozure/ccl/issues/111#issuecomment-464609012, or mute the thread https://github.com/notifications/unsubscribe-auth/AFKzKaxac-kx2FeXOAPCyLffF93fajDZks5vOk7TgaJpZM4SRYCz .
I am a mere observer, but it's been 10 days and I would like not to see this feature stalled on completion for months or years or decades... (And I think this man has well earned his damn 260$.)
Surely at this point, if any remaining issues were to be detected after delivery, they should be fairly easy to fix anyway, right?
Personally, I've been wishing for portable package-local nicknames for years, it would be a nice addition to the landscape and maybe it would kickstart a new wave of language-level improvements...
@Hexstream There is still work to be done. The package-local nicknames tests still need to be extended and run against CCL and other implementations. See https://github.com/Clozure/ccl/pull/188#issuecomment-465220576
@pfdietz @xrme @MattKaufmann Since I submitted a bounty claim on Bountysource, I have no idea how I should split the bounty now that it's been a team effort. You also deserve your share for helping test the hell out of it and helping me from maintainers' point of view.
@phoe That's kind of you to offer, but no bounty for me, thank you.
I'm very glad to see this was finally merged.
@phoe If you did 70%+ of the job, just run away with the money and see if someone tackles you. ;P
No bounty money for me either.
On Wed, Apr 17, 2019, 10:32 AM Jean-Philippe Paradis < notifications@github.com> wrote:
I'm very glad to see this was finally merged.
@phoe https://github.com/phoe If you did 70%+ of the job, just run away with the money and see if someone tackles you. ;P
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/Clozure/ccl/issues/111#issuecomment-484115540, or mute the thread https://github.com/notifications/unsubscribe-auth/ATLrtrSq4qdmJ2IkkR5DY507O8-nOTeiks5vhzB7gaJpZM4SRYCz .
Thank you @phoe, but there's no need to share any of the bounty funds with me.
Thank you, everyone.
There are still two test-related tasks to do: the additional tests mentioned by @pfdietz, and perhaps including the PLN test suite in CCL's base test suite. Should these get separate GitHub issues? -- Wysłane za pomocą K-9 Mail.
Yes, I think so.
On Wed, Apr 17, 2019, 12:16 PM Michał Herda notifications@github.com wrote:
Thank you, everyone.
There are still two test-related tasks to do: the additional tests mentioned by @pfdietz, and perhaps including the PLN test suite in CCL's base test suite. Should these get separate GitHub issues? -- Wysłane za pomocą K-9 Mail.
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/Clozure/ccl/issues/111#issuecomment-484158937, or mute the thread https://github.com/notifications/unsubscribe-auth/ATLrtvzaE5Mzw6-2FSG3kmSLJvm3U1rsks5vh0jegaJpZM4SRYCz .
Done over at the pln-tests repository:
https://github.com/phoe/package-local-nicknames-tests/issues/3 https://github.com/phoe/package-local-nicknames-tests/issues/4
I'm getting a stack overflow with package-local-nicknames; please see Issue #207.
Three Common Lisp implementations (SBCL, ECL, and ABCL) have adopted an extension to defpackage, :local-nicknames. This extension helps solve the serious problem of package (and, in particular, nickname) collisions between different CL libraries. If CCL (and, perhaps, CLISP) adopt this extension also, then the system on quicklisp can be encouraged to use it and avoid most of the collisions that currently plague it.
The syntax is:
(:local-nicknames (nickname package) ...)
where nickname is a designator for a nickname, and package a designator for a package name.
When package is bound to a package that has local nicknames, the reader recognizes the local nicknames in that package as mapping to the corresponding actual packages. The printer is allowed to use local nicknames when package allows it to, but is not required to (it may use real package names instead).