{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/271","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/271/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/271/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/271/events","html_url":"https://github.com/FStarLang/FStar/issues/271","id":91091522,"number":271,"title":"we should deprecate old libraries","user":{"login":"markulf","id":9845640,"avatar_url":"https://avatars.githubusercontent.com/u/9845640?v=3","gravatar_id":"","url":"https://api.github.com/users/markulf","html_url":"https://github.com/markulf","followers_url":"https://api.github.com/users/markulf/followers","following_url":"https://api.github.com/users/markulf/following{/other_user}","gists_url":"https://api.github.com/users/markulf/gists{/gist_id}","starred_url":"https://api.github.com/users/markulf/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/markulf/subscriptions","organizations_url":"https://api.github.com/users/markulf/orgs","repos_url":"https://api.github.com/users/markulf/repos","events_url":"https://api.github.com/users/markulf/events{/privacy}","received_events_url":"https://api.github.com/users/markulf/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-06-25T22:20:40Z","updated_at":"2015-06-27T06:40:47Z","closed_at":null,"body":"Many examples still use old libraries. We should port the examples one by one, and clearly mark the libraries as deprecated, so no one uses them for new verification projects. Should we have a `deprecated` folder in the `lib` folder, mirroring the `to_be_ported` folder in the `exercise` folder?\r\n\r\n`Array.fst` defines `seq` and seems to be replaced by `Seq.fst` and `SeqProperties.fst` and is used in the following examples:\r\n\r\n``` \r\nalgorithms/downgrade.fst\r\nalgorithms/qsort_arr.fst \r\nbignum/eval_st.fst \r\nbug-reports/bug151.fst \r\ncrypto/acls-cap.fst\r\ncrypto/cert.fst\r\ncrypto/cnt-format.fst\r\ncrypto/encrypt.fst\r\ncrypto/encrypt2.fst\r\ncrypto/encrypt3.fst\r\ncrypto/format.fst\r\ncrypto/hybrid.fst\r\ncrypto/hybrid2.fst\r\ncrypto/mac.fst\r\ncrypto/mac3.fst\r\ncrypto/padding.fst\r\ncrypto/rpc.fst\r\ncrypto/rpc2.fst\r\ncrypto/sig.fst\r\nto_be_ported/misc/ringbuffer.fst\r\nto_be_ported/monadic/sparseArray0-1.fst\r\nto_be_ported/monadic/sparseArray0.fst\r\nto_be_ported/sep/rbsep.fst\r\nto_be_ported/sep/rbsep.fst\r\nto_be_ported/sep/rbsep2.fst\r\nto_be_ported/sep/rbsep2.fst\r\nunit-tests/certsig.fst\r\nunit-tests/mac2.fst\r\n```\r\n\r\n`partialmap.fst` defines modules `Set`, `Map`, `Heap`, `Array` and appears in \r\n\r\n```\r\ncrypto/cnt-format.fst\r\ncrypto/format.fst\r\ncrypto/Makefile\r\n```"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/115975216","html_url":"https://github.com/FStarLang/FStar/issues/271#issuecomment-115975216","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/271","id":115975216,"user":{"login":"beurdouche","id":1193431,"avatar_url":"https://avatars.githubusercontent.com/u/1193431?v=3","gravatar_id":"","url":"https://api.github.com/users/beurdouche","html_url":"https://github.com/beurdouche","followers_url":"https://api.github.com/users/beurdouche/followers","following_url":"https://api.github.com/users/beurdouche/following{/other_user}","gists_url":"https://api.github.com/users/beurdouche/gists{/gist_id}","starred_url":"https://api.github.com/users/beurdouche/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/beurdouche/subscriptions","organizations_url":"https://api.github.com/users/beurdouche/orgs","repos_url":"https://api.github.com/users/beurdouche/repos","events_url":"https://api.github.com/users/beurdouche/events{/privacy}","received_events_url":"https://api.github.com/users/beurdouche/received_events","type":"User","site_admin":false},"created_at":"2015-06-27T06:40:47Z","updated_at":"2015-06-27T06:40:47Z","body":"I suggest maybe we could associate a status info to each file to know wether it is\r\n- Stable\r\n- InConstruction (or whatever...)\r\n- Deprecated\r\n\r\nThen we can review the deprecated one, check that everything has been ported to the new one and cleanup when ready."}}