{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/1444","repository_url":"https://api.github.com/repos/FStarLang/FStar","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/1444/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/1444/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/1444/events","html_url":"https://github.com/FStarLang/FStar/issues/1444","id":319228187,"number":1444,"title":"--already_cached: A new flag for the dependence analysis","user":{"login":"nikswamy","id":6163359,"avatar_url":"https://avatars0.githubusercontent.com/u/6163359?v=4","gravatar_id":"","url":"https://api.github.com/users/nikswamy","html_url":"https://github.com/nikswamy","followers_url":"https://api.github.com/users/nikswamy/followers","following_url":"https://api.github.com/users/nikswamy/following{/other_user}","gists_url":"https://api.github.com/users/nikswamy/gists{/gist_id}","starred_url":"https://api.github.com/users/nikswamy/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nikswamy/subscriptions","organizations_url":"https://api.github.com/users/nikswamy/orgs","repos_url":"https://api.github.com/users/nikswamy/repos","events_url":"https://api.github.com/users/nikswamy/events{/privacy}","received_events_url":"https://api.github.com/users/nikswamy/received_events","type":"User","site_admin":false},"labels":[{"id":326272051,"url":"https://api.github.com/repos/FStarLang/FStar/labels/component/build","name":"component/build","color":"c5def5","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2018-05-01T15:19:15Z","updated_at":"2018-05-04T19:39:46Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"Aiming to solve a few problems with build and dependency analysis\r\n\r\n1. An F* project should be able to build itself; another project that\r\n   depends on it should not have to try to build it again (and get it\r\n   wrong)\r\n\r\n2. Concurrent builds should be possible, so long as they avoid racing\r\n   to write the same .checked file; mechanisms to ensure that a build\r\n   can fail if a .checked file isn't present would be useful.\r\n\r\n3. We should be able to build a project given only .checked files for\r\n   its dependences.\r\n\r\n4. With use_extracted_interfaces, we can shrink the dependences of a\r\n   project to only the dependences of the interfaces it depends on.\r\n\r\nPoints 1 and 2 are already possible with the current support\r\navailable, but it can be a bit cumbersome and may require recursive\r\ninvocations of make.\r\n\r\n## Proposal: A new F* option `--already_cached <namespace selector>`\r\n\r\nwhere `<namespace selector>` is a string like `FStar MiTLS.LowParse`\r\nor `* -MiTLS` etc., which can be used to select or deselect one or\r\nmore namespaces / module names.\r\n\r\n### Dependence analysis\r\n\r\n1. `fstar --dep full --already_cached ns ROOTS` will scan starting from\r\n   ROOTS, as usual.\r\n\r\n2. When it finds a dependence on module `M` that matches `ns`, rather\r\n   than searching for `M.fst(i)` it searches for `M.fst(i).checked` in\r\n   the include path. Say it finds it at path\r\n   `<path_to_M>/M.fst.checked`\r\n\r\n3. Having found the M.fst.checked file, it computes the immediate\r\n   dependeces of `M` by just reading it from the list of immediate\r\n   dependences of recorded in the interface section of the .checked\r\n   file. \r\n\r\n   -- If any of those immediate dependences does not match the\r\n      namespace selector `ns`, the dependence analysis fails with an\r\n      error requesting to add that module to the namespace selector.\r\n\r\n   -- While .checked files have an interface section, they do not yet contain interface dependences separately from module dependences. This would also have to be added.\r\n\r\n4. It adds those immediate dependences to the set of pending modules\r\n   to be scanned and continues.\r\n\r\n5. The final output of the dependence analysis includes Makefile\r\n   dependence rules only for those modules whose names do not match\r\n   <ns>. For example, it will contain:\r\n\r\n   ```A.fst.checked: A.fst <path_to_M>/M.fst.checked```\r\n\r\n   But it will not contain such a rule for `M.fst.checked`.\r\n\r\n6. The dependence analysis also defines three variables:\r\n\r\n   * ALL_FST_FILES: This will contain all .fst and .fsti files\r\n     encountered in the scan (i.e., excluding all the .checked files)\r\n\r\n   * ALL_ML_FILES: This will contain .ml file names for all *modules*\r\n     encountered in the scan, including .fst and .checked versions,\r\n     subject to the \"--extract <namespace selector>\" feature. For a\r\n     checked file, say, `<path_to_M>/M.fst.checked`, the dependence\r\n     analysis will search for `M.ml` in the include path and emit\r\n     `<path_to_M.ml>/M.ml`.\r\n\r\n   * ALL_KRML_FILES: This behaves the same as for .ml files, except\r\n     using .krml files. Additionally, since KreMLin is a full-program\r\n     analysis, we include all .krml files, disregarding the `--extract\r\n     <namespace selector>`.\r\n\r\n### Verification runs of F*\r\n\r\n1. `fstar --already_cached ns ROOTS` will run the dependence analysis\r\n   as in the previous section.\r\n\r\n2. F* will then load a set of .checked files as dictated by the\r\n   dependence analysis, and for any .checked file that is in <ns>, F*\r\n   will load the .checked file (it must exist, since otherwise the\r\n   dependence analysis would have already failed).\r\n\r\n   a. When loading M.fst.checked, if M.fst is found in the include\r\n   path, F* will check the digest stored in M.fst.checked for\r\n   consistency with M.fst (and its dependences).\r\n\r\n   b. If M.fst is not found, F* will load the checked file without\r\n   checking a digest."},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/386711607","html_url":"https://github.com/FStarLang/FStar/issues/1444#issuecomment-386711607","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/1444","id":386711607,"user":{"login":"nikswamy","id":6163359,"avatar_url":"https://avatars0.githubusercontent.com/u/6163359?v=4","gravatar_id":"","url":"https://api.github.com/users/nikswamy","html_url":"https://github.com/nikswamy","followers_url":"https://api.github.com/users/nikswamy/followers","following_url":"https://api.github.com/users/nikswamy/following{/other_user}","gists_url":"https://api.github.com/users/nikswamy/gists{/gist_id}","starred_url":"https://api.github.com/users/nikswamy/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nikswamy/subscriptions","organizations_url":"https://api.github.com/users/nikswamy/orgs","repos_url":"https://api.github.com/users/nikswamy/repos","events_url":"https://api.github.com/users/nikswamy/events{/privacy}","received_events_url":"https://api.github.com/users/nikswamy/received_events","type":"User","site_admin":false},"created_at":"2018-05-04T19:39:46Z","updated_at":"2018-05-04T19:39:46Z","author_association":"CONTRIBUTOR","body":"> But we could also just bail out entirely (that's what Coq does: it never looks for .v files as dependencies).\r\n\r\nThe option is to provide this behavior. It's exactly what we had in mind in discussions with @tahina-pro \r\n "}}
{"actor":{"display_login":"nikswamy"}}