Check discouraged #91
Conversation
This adds, to the Travis checks, a check that the "discouraged" results are as expected. This way, if anyone modifies the results (e.g., by using a theorem whose use is discouraged), it will be immediately noted. This adds a new file, "discouraged", that contains the *expected* results of "show discouraged" with some minor reformatting. It also adds a Travis check that when regenerated, the same results occur. The results are sorted, so that benign movement won't trigger a problem. If you *do* intend to change what is discouraged or the use of them, just regenerate the "discouraged" file using the instructions in .travis.yml.
|
Per the recent email discussion, this checks to see if the "show discouraged" results have changed. I sort the results, so that things can move around without problems. |
|
Keep in mind that 'show discouraged' takes a minute or so to run, so it
will probably be the slowest thing in the Travis script. This may or
may not be a problem but is something to keep in mind if Travis run time
becomes a concern.
The slow speed is primarily due to 4200 internal 'show usage' calls and
could probably be made more efficient with a better algorithm, but I
don't have that as an urgent item on my to-do list right now.
Norm
…On 12/28/16 10:23 PM, David A. Wheeler wrote:
Per the recent email discussion, this checks to see if the "show
discouraged" results have changed.
I sort the results, so that things can move around without problems.
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<#91 (comment)>, or
mute the thread
<https://github.com/notifications/unsubscribe-auth/AMKLqAapw0uFNwC-KQM9V5WRFeAAk_3-ks5rMyehgaJpZM4LXUy3>.
|
|
@nmegill I added a new macro to mmj2, |
|
It takes around 20s torun locally. Not the slowest step, but noticeable. I can switch to mmj2. |
|
@david-a-wheeler I added an extra line |
|
How do you invoke showDiscouraged? Alternatively, can you just midify .travis.yml to use it?? Please leave a comment behind on how to do it with metanath.exe. |
|
Already done, see 7414a93...88a943f . Basically, you add the line to your RunParms, as mentioned above; there is an optional argument which controls the output folder and filename. It is already sorted and the wording matches metamath.exe, so it can be sent straight to |
|
In c580c44..d1fafc8 I added usage discouraged tags to 416 *ENF theorems
to prevent them from being used by 'minimize'. So Travis should list
them as well as all of their current uses.
BTW where do I look at the Travis output, and is it possible to have it
emailed to me iff an error is reported?
Norm
…On 12/29/16 8:56 AM, Mario Carneiro wrote:
Already done, see 7414a93...88a943f
<7414a93...88a943f>
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#91 (comment)>, or
mute the thread
<https://github.com/notifications/unsubscribe-auth/AMKLqP0a_dIgjeIamkccUxRJqYc-IKY_ks5rM7v7gaJpZM4LXUy3>.
|
|
OK, I see where to find the Travis output now.
The failure in my earlier 88a943f..c580c44 is interesting: The uses of
bnj524 (which has usage discouraged) decreased from 21 to 20 as a result
of the minimization run. This is the opposite of an error (fewer uses
are generally good). But I think it's OK to report that since it can be
useful information, such as letting us know that a *OLD is ready to be
deleted when its usage falls to 0.
One thing to think about is changing the "diff -u" to "diff -U 0" to
reduce irrelevant lines in the diff, since each line is independent and
the surrounding lines are just "noise" because they do not represent any
particular context.
Norm
…On 12/29/16 7:09 PM, ***@***.*** wrote:
In c580c44..d1fafc8 I added usage discouraged tags to 416 *ENF theorems
to prevent them from being used by 'minimize'. So Travis should list
them as well as all of their current uses.
BTW where do I look at the Travis output, and is it possible to have it
emailed to me iff an error is reported?
|
|
The travis log itself is not emailed to you, but you should get an email
from Travis saying that the build failed, with a link to the log.
…On Thu, Dec 29, 2016 at 7:09 PM, nmegill ***@***.***> wrote:
In c580c44..d1fafc8 I added usage discouraged tags to 416 *ENF theorems
to prevent them from being used by 'minimize'. So Travis should list
them as well as all of their current uses.
BTW where do I look at the Travis output, and is it possible to have it
emailed to me iff an error is reported?
Norm
On 12/29/16 8:56 AM, Mario Carneiro wrote:
> Already done, see 7414a93...88a943f
> <7414a93...88a943f>
>
> —
> You are receiving this because you were mentioned.
> Reply to this email directly, view it on GitHub
> <#91 (comment)>, or
> mute the thread
> <https://github.com/notifications/unsubscribe-auth/AMKLqP0a_
dIgjeIamkccUxRJqYc-IKY_ks5rM7v7gaJpZM4LXUy3>.
>
—
You are receiving this because you modified the open/close state.
Reply to this email directly, view it on GitHub
<#91 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/AA1A7M1FSMd8UBJVzMCqDIb7zbLv3qa6ks5rNEvGgaJpZM4LXUy3>
.
|
|
I have never received such an email. Where do I go to set this up?
Norm
…On 12/29/16 9:27 PM, Mario Carneiro wrote:
The travis log itself is not emailed to you, but you should get an email
from Travis saying that the build failed, with a link to the log.
|
The "-u" is useful if someone is thinking about adding the lines "by hand", but in retrospect, that's extremely unlikely. I think we should do that. |
No description provided.