{"action":"closed","issue":{"url":"https://api.github.com/repos/RedPRL/redtt/issues/392","repository_url":"https://api.github.com/repos/RedPRL/redtt","labels_url":"https://api.github.com/repos/RedPRL/redtt/issues/392/labels{/name}","comments_url":"https://api.github.com/repos/RedPRL/redtt/issues/392/comments","events_url":"https://api.github.com/repos/RedPRL/redtt/issues/392/events","html_url":"https://github.com/RedPRL/redtt/issues/392","id":369774633,"node_id":"MDU6SXNzdWUzNjk3NzQ2MzM=","number":392,"title":"Informal description of the rot files","user":{"login":"favonia","id":1471328,"node_id":"MDQ6VXNlcjE0NzEzMjg=","avatar_url":"https://avatars1.githubusercontent.com/u/1471328?v=4","gravatar_id":"","url":"https://api.github.com/users/favonia","html_url":"https://github.com/favonia","followers_url":"https://api.github.com/users/favonia/followers","following_url":"https://api.github.com/users/favonia/following{/other_user}","gists_url":"https://api.github.com/users/favonia/gists{/gist_id}","starred_url":"https://api.github.com/users/favonia/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/favonia/subscriptions","organizations_url":"https://api.github.com/users/favonia/orgs","repos_url":"https://api.github.com/users/favonia/repos","events_url":"https://api.github.com/users/favonia/events{/privacy}","received_events_url":"https://api.github.com/users/favonia/received_events","type":"User","site_admin":false},"labels":[{"id":973333592,"node_id":"MDU6TGFiZWw5NzMzMzM1OTI=","url":"https://api.github.com/repos/RedPRL/redtt/labels/Thought","name":"Thought","color":"b7f97c","default":false}],"state":"closed","locked":false,"assignee":{"login":"favonia","id":1471328,"node_id":"MDQ6VXNlcjE0NzEzMjg=","avatar_url":"https://avatars1.githubusercontent.com/u/1471328?v=4","gravatar_id":"","url":"https://api.github.com/users/favonia","html_url":"https://github.com/favonia","followers_url":"https://api.github.com/users/favonia/followers","following_url":"https://api.github.com/users/favonia/following{/other_user}","gists_url":"https://api.github.com/users/favonia/gists{/gist_id}","starred_url":"https://api.github.com/users/favonia/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/favonia/subscriptions","organizations_url":"https://api.github.com/users/favonia/orgs","repos_url":"https://api.github.com/users/favonia/repos","events_url":"https://api.github.com/users/favonia/events{/privacy}","received_events_url":"https://api.github.com/users/favonia/received_events","type":"User","site_admin":false},"assignees":[{"login":"favonia","id":1471328,"node_id":"MDQ6VXNlcjE0NzEzMjg=","avatar_url":"https://avatars1.githubusercontent.com/u/1471328?v=4","gravatar_id":"","url":"https://api.github.com/users/favonia","html_url":"https://github.com/favonia","followers_url":"https://api.github.com/users/favonia/followers","following_url":"https://api.github.com/users/favonia/following{/other_user}","gists_url":"https://api.github.com/users/favonia/gists{/gist_id}","starred_url":"https://api.github.com/users/favonia/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/favonia/subscriptions","organizations_url":"https://api.github.com/users/favonia/orgs","repos_url":"https://api.github.com/users/favonia/repos","events_url":"https://api.github.com/users/favonia/events{/privacy}","received_events_url":"https://api.github.com/users/favonia/received_events","type":"User","site_admin":false}],"milestone":null,"comments":1,"created_at":"2018-10-13T06:57:35Z","updated_at":"2018-10-20T11:28:57Z","closed_at":"2018-10-20T11:28:57Z","author_association":"COLLABORATOR","body":"The *rot* format is to store elaborated (and 99% normalized) redtt definitions to speed up imports. A *rot* file is a YAML file consisting of four sections:\r\n\r\n0. file format version\r\n1. dependencies\r\n2. resource imports\r\n3. resource\r\n\r\nThis is assuming `redlib` cannot change the semantics of `red` or `rot` files in any way.\r\n\r\n---\r\n\r\nThe file format version section is\r\n```yaml\r\nversion: 0\r\n```\r\nwhich denotes the format version of this *rot* file.\r\n\r\n---\r\n\r\nThe dependency section is\r\n```yaml\r\ndeps:\r\n- method: redsum\r\n  params:\r\n  - 372cd79a70ea07d2b4d82a4ee320a2c5\r\n- method: rotsum\r\n  params:\r\n  - fun\r\n  - d860de4a96da39d24047d8fe68eb2d39\r\n- method: rotsum\r\n  params:\r\n  - nat\r\n  - 8002bb15defde74ee7e5fd4c5539ec0f\r\n```\r\nwhere each item describes a precondition. Only when all the preconditions hold a *rot* file is considered usable. `method` refers to a hook supported by the dependency checker and `params` are the parameters fed into the hook. Currently, in version 0, the following hooks are supported:\r\n\r\n- `false`: always false.\r\n- `true`: always true.\r\n- `redsum [hash]`: true if the checksum of the corresponding `red` file is `hash`.\r\n- `rotsum [selector, hash]`: true if the checksum of the corresponding `red` file is `hash`.\r\n- `shell [cmd, output]`: run the command `cmd` through `system` and compare its output with `output`.\r\n\r\n---\r\n\r\nThe resource imports section is\r\n```yaml\r\nimports:\r\n- type: rot\r\n  params: [\"fun\"]\r\n  children:\r\n  - type: rot\r\n    params: [\"base\"]\r\n    children: []\r\n- type: rot\r\n  params: [\"nat\"]\r\n  children: []\r\n```\r\nwhich gives a list of other resources that can be accessed from the resource section. It is assumed that there is no self-importing or other cyclic references. The resource section should be self-contained except for possible references to some resource listed in this section. Currently, the only supported type is `rot`, which is to generate a `rot` file from a `red` file (if non-existing or unusable) and import its content.\r\n\r\n---\r\n\r\nFinally, the resource section is\r\n```yaml\r\ndata:\r\n- type: def\r\n  params:\r\n  - id\r\n  - \"(pi (U kan) [0] (pi 0 [1] 0))\"\r\n  - \"(lookup (0 1) id)\"\r\n- type: data\r\n  params:\r\n  - s1\r\n  - ...\r\n- type: opaque def\r\n  params:\r\n  - magic\r\n  - \"(path [0] (lookup (1) nat) (lookup (1) zero) ((lookup (1) suc) (lookup (1) zero))\"\r\n```\r\nwhich intends to store the fully elaborated redtt signatures. The exact format is work in progress. Note that the resource section *must be self-contained* except for possible references to the resources listed in the \"imports\" section. The reference format is `(lookup (num+) string*)` which would look up the resource.\r\n\r\n---\r\n\r\nNecessary changes to the current framework.\r\n\r\n0. The elaborator should not control the import procedure. Instead, the elaborator should be a routine under the control of another module orchestrating the entire compilation process."}}
{"actor":{"display_login":"favonia"}}