{"action":"created","issue":{"url":"https://api.github.com/repos/metamath/set.mm/issues/59","repository_url":"https://api.github.com/repos/metamath/set.mm","labels_url":"https://api.github.com/repos/metamath/set.mm/issues/59/labels{/name}","comments_url":"https://api.github.com/repos/metamath/set.mm/issues/59/comments","events_url":"https://api.github.com/repos/metamath/set.mm/issues/59/events","html_url":"https://github.com/metamath/set.mm/issues/59","id":164237674,"number":59,"title":"\"SHOW RESTRICTED\" in Travis","user":{"login":"digama0","id":868588,"avatar_url":"https://avatars.githubusercontent.com/u/868588?v=3","gravatar_id":"","url":"https://api.github.com/users/digama0","html_url":"https://github.com/digama0","followers_url":"https://api.github.com/users/digama0/followers","following_url":"https://api.github.com/users/digama0/following{/other_user}","gists_url":"https://api.github.com/users/digama0/gists{/gist_id}","starred_url":"https://api.github.com/users/digama0/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/digama0/subscriptions","organizations_url":"https://api.github.com/users/digama0/orgs","repos_url":"https://api.github.com/users/digama0/repos","events_url":"https://api.github.com/users/digama0/events{/privacy}","received_events_url":"https://api.github.com/users/digama0/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/metamath/set.mm/labels/maintenance","name":"maintenance","color":"fbca04"},{"url":"https://api.github.com/repos/metamath/set.mm/labels/meta","name":"meta","color":"b60205"}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":11,"created_at":"2016-07-07T06:21:00Z","updated_at":"2016-07-07T18:24:29Z","closed_at":null,"body":"The latest version of metamath.exe includes a command SHOW RESTRICTED that will allow us to verify that (New usage/Proof modification is discouraged.) marks are honored. Norm writes:\r\n\r\n> I finished implementing the \"is discouraged\" markup in metamath.exe and will release it after some more testing.\r\n\r\n> For comparing set.mm to previous versions, I decided against reading two files in metamath.exe because I think external scripting of the diff can provide more flexibility.  A new command, \"show restricted\", simply lists all statements containing the \"discouraged\" comment markup for diff comparison with a previous set.mm.  I think you mentioned this was sufficient for a travis script.\r\n\r\n> Comparing proofs is somewhat problematic because changing labels and reordering hypotheses can make them mismatch completely.  One thing that is constant is the number of steps, so I am listing that instead of the actual proof.  In practice, I think this is sufficient to detect 99.99% of overridden proofs because it seems very unlikely that a revised proof would have exactly the same number of steps.  For the use case I'm most concerned about, minimize_with, the number of steps would always be different.\r\n\r\n> Here is a sample session.  I prefixed each line with the string \"SHOW RESTRICTED:\"  for easy identification of the lines with a script.\r\n\r\n> To make diff results easier to interpret, I am listing each usage on a new line with both the original statement and its target.\r\n\r\n> --- begin sample session ---\r\n\r\n>     MM> help show restricted\r\n>     Syntax:  SHOW RESTRICTED\r\n>     \r\n>     This command shows the usage and proof statistics of statements with\r\n>     \"(Proof modification is discouraged.)\" and \"(New usage is\r\n>     discouraged.)\" markup tags in their description comments.  The output\r\n>     is intended to be used by scripts that compare a modified .mm file\r\n>     to a previous version.\r\n>     \r\n>     MM> show restricted\r\n>     SHOW RESTRICTED:  Proof of \"id1\" is restricted (26 steps).\r\n>     SHOW RESTRICTED:  Proof of \"dfbi1gb\" is restricted (100 steps).\r\n>     SHOW RESTRICTED:  Proof of \"jcabOLD\" is restricted (42 steps).\r\n>     SHOW RESTRICTED:  Usage of \"jcabOLD\" is restricted (0 uses).\r\n>     SHOW RESTRICTED:  Proof of \"pm3.43OLD\" is restricted (17 steps).\r\n>     SHOW RESTRICTED:  Usage of \"pm3.43OLD\" is restricted (0 uses).\r\n>     SHOW RESTRICTED:  Proof of \"con3th\" is restricted (65 steps).\r\n>     SHOW RESTRICTED:  Proof of \"tru2OLD\" is restricted (9 steps).\r\n>     SHOW RESTRICTED:  Usage of \"tru2OLD\" is restricted (0 uses).\r\n>     SHOW RESTRICTED:  Usage of \"ax-meredith\" is restricted (13 uses).\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem1\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem2\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem1\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem2\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem3\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem4\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem5\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem7\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem8\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem9\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem10\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem11\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"merlem13\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"luk-1\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"luk-2\".\r\n>     SHOW RESTRICTED:  \"ax-meredith\" is used by \"luk-2\".\r\n>     SHOW RESTRICTED:  Proof of \"merlem1\" is restricted (62 steps).\r\n>     SHOW RESTRICTED:  Usage of \"merlem1\" is restricted (3 uses).\r\n>     SHOW RESTRICTED:  \"merlem1\" is used by \"merlem2\".\r\n>     SHOW RESTRICTED:  \"merlem1\" is used by \"merlem5\".\r\n>     ......  etc. .............\r\n\r\nThis command can easily be converted to a usage generator script:\r\n\r\n     ./metamath 'read set.mm' 'show restricted' exit | grep 'SHOW RESTRICTED' > set.usage\r\n\r\nwill calculate the usage in `set.mm` and output it to `set.usage`. Treated as a function from mm files to usage files, whenever a change is introduced that changes the usage output, this change ought to be marked as \"override\" or something similar.\r\n\r\nThe problem is that Travis is not designed for evaluating a build in the context of previous builds. It's not that it's impossible - it's as simple as checking out the `HEAD^` version of set.mm and comparing the generated `set.usage` files. But if this fails, it represents a non-repeatable \"error\", since pushing the exact same commit a second time will resolve the failure.\r\n\r\nOne way to solve this is to store the usage file in the repo. Then the correctness check that can be performed by Travis is that the generated usage matches the stored usage file, and the equivalent of an \"override\" in this context is an update to the usage file in the commit using the above command. This does mean that anyone who is not capable of running this command (adapted for their platform) will not be able to override usage checks, but this seems like a reasonable compromise.\r\n\r\nThoughts?"},"comment":{"url":"https://api.github.com/repos/metamath/set.mm/issues/comments/231165022","html_url":"https://github.com/metamath/set.mm/issues/59#issuecomment-231165022","issue_url":"https://api.github.com/repos/metamath/set.mm/issues/59","id":231165022,"user":{"login":"sorear","id":92735,"avatar_url":"https://avatars.githubusercontent.com/u/92735?v=3","gravatar_id":"","url":"https://api.github.com/users/sorear","html_url":"https://github.com/sorear","followers_url":"https://api.github.com/users/sorear/followers","following_url":"https://api.github.com/users/sorear/following{/other_user}","gists_url":"https://api.github.com/users/sorear/gists{/gist_id}","starred_url":"https://api.github.com/users/sorear/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/sorear/subscriptions","organizations_url":"https://api.github.com/users/sorear/orgs","repos_url":"https://api.github.com/users/sorear/repos","events_url":"https://api.github.com/users/sorear/events{/privacy}","received_events_url":"https://api.github.com/users/sorear/received_events","type":"User","site_admin":false},"created_at":"2016-07-07T18:24:29Z","updated_at":"2016-07-07T18:24:29Z","body":"```\r\n&& [ `egrep -q '?Error|?Warning' < mm.log; echo $?` -eq 1 ]\r\n```\r\n\r\nCan't this be better written as:\r\n\r\n```\r\n&& ! grep -qE '?Error|?Warning' mm.log\r\n```\r\n\r\nThere's no need to drag `$?` into this, plain old status negation works; `grep` takes a filename as an argument; and `egrep` is vaguely deprecated in favor of `grep -E` …"}}
{"actor":{"display_login":"sorear"}}