{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/473","repository_url":"https://api.github.com/repos/FStarLang/FStar","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/473/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/473/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/473/events","html_url":"https://github.com/FStarLang/FStar/issues/473","id":131168296,"number":473,"title":"Weird issue with seq.fsi / FStar.Seq.fst","user":{"login":"msprotz","id":10673049,"avatar_url":"https://avatars.githubusercontent.com/u/10673049?v=3","gravatar_id":"","url":"https://api.github.com/users/msprotz","html_url":"https://github.com/msprotz","followers_url":"https://api.github.com/users/msprotz/followers","following_url":"https://api.github.com/users/msprotz/following{/other_user}","gists_url":"https://api.github.com/users/msprotz/gists{/gist_id}","starred_url":"https://api.github.com/users/msprotz/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/msprotz/subscriptions","organizations_url":"https://api.github.com/users/msprotz/orgs","repos_url":"https://api.github.com/users/msprotz/repos","events_url":"https://api.github.com/users/msprotz/events{/privacy}","received_events_url":"https://api.github.com/users/msprotz/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2016-02-03T22:02:12Z","updated_at":"2016-02-04T09:30:30Z","closed_at":null,"body":"It seems like FStar.Seq.fst cannot be verified alone, and needs seq.fsi prepended to it... this is sending the auto-deps analysis off the rails. Any way we can get rid of seq.fsi?"},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/179730262","html_url":"https://github.com/FStarLang/FStar/issues/473#issuecomment-179730262","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/473","id":179730262,"user":{"login":"catalin-hritcu","id":5850655,"avatar_url":"https://avatars.githubusercontent.com/u/5850655?v=3","gravatar_id":"","url":"https://api.github.com/users/catalin-hritcu","html_url":"https://github.com/catalin-hritcu","followers_url":"https://api.github.com/users/catalin-hritcu/followers","following_url":"https://api.github.com/users/catalin-hritcu/following{/other_user}","gists_url":"https://api.github.com/users/catalin-hritcu/gists{/gist_id}","starred_url":"https://api.github.com/users/catalin-hritcu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/catalin-hritcu/subscriptions","organizations_url":"https://api.github.com/users/catalin-hritcu/orgs","repos_url":"https://api.github.com/users/catalin-hritcu/repos","events_url":"https://api.github.com/users/catalin-hritcu/events{/privacy}","received_events_url":"https://api.github.com/users/catalin-hritcu/received_events","type":"User","site_admin":false},"created_at":"2016-02-04T09:30:30Z","updated_at":"2016-02-04T09:30:30Z","body":"On Thu, Feb 4, 2016 at 10:28 AM, Zinzindohoué Jean Karim <\nnotifications@github.com> wrote:\n\n> You can merge seq.fsi into FStar.Seq.fst and rename seq.fsi into\n> FStar.Seq.fsi.\n> I do not know what Set was renamed but not Seq.\n\n\nToo many typos in this comment? Makes little sense to me.\n\n\n>\n>\n> 2016-02-03 23:03 GMT+01:00 Jonathan Protzenko <notifications@github.com>:\n>\n> > There seems to be a similar issue with ordset.fsi:\n> >\n> > protz@Joprotze-Z420:~/Code/fstar/examples/algorithms (master) $ fstar\n> --explicit_deps --admit_fsi FStar.Set --admit_fsi FStar.OrdSet --admit_fsi\n> FStar.OrdSetPropsFStar.FunctionalExtensionality.fst FStar.Set.fsi\n> FStar.Heap.fst FStar.ST.fst FStar.All.fst FStar.List.Tot.fst ordset.fsi\n> FStar.OrdSetProps.fst unification.fst\n> > Verifying module: FStar.Heap\n> > Verifying module: FStar.ST\n> > Verifying module: FStar.All\n> > Verifying module: FStar.List.Tot\n> > Verifying module: FStar.OrdSetProps\n> > Verifying module: Unification\n> > All verification conditions discharged successfully\n> > protz@Joprotze-Z420:~/Code/fstar/examples/algorithms (master) $ fstar\n> --dep nubuild !$\n> > fstar --dep nubuild unification.fst\n> > D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\prims.fst\n> > D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\FStar.Set.fsi\n> > D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\FStar.Heap.fst\n> > D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\FStar.ST.fst\n> > D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\FStar.All.fst\n> > D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\FStar.List.Tot.fst\n> > D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\FStar.List.fst\n> > D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\FStar.OrdSet.fst\n> > unification.fst\n> > protz@Joprotze-Z420:~/Code/fstar/examples/algorithms (master) $ fstar\n> unification.fst\n> > D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\FStar.OrdSet.fst(58,6-58,46) : Error\n> > (D:\\cygwin\\home\\protz\\Code\\fstar\\lib\\FStar.OrdSet.fst(58,6-58,46))\n> Failed to solve the sub-problem\n> > (U18905 a f s1 s2 hd tl) (Typ_app(Typ_uvar, [6 args]))\n> > =(TOP)\n> > l:(ordset a f){((is_Cons l) /\\ (((hd l) = x) \\/ ((is_Cons s) /\\ ((hd l)\n> = (hd s)))))} (Typ_refine) (guard (U18906 a f s1 s2 hd tl))\n> > Which arose because:\n> > TOP\n> > Failed because:free-variable check failed on a non-redex\n> >\n> > —\n> > Reply to this email directly or view it on GitHub\n> > <https://github.com/FStarLang/FStar/issues/473#issuecomment-179493891>.\n>\n> >\n>\n> —\n> Reply to this email directly or view it on GitHub\n> <https://github.com/FStarLang/FStar/issues/473#issuecomment-179729361>.\n>\n"}}