技术控

    今日:0| 主题:63445
收藏本版 (1)
最新软件应用技术尽在掌握

[其他] Towards Idris Version 1.0

[复制链接]
蹲街角只为等待伱 发表于 2016-11-30 21:20:07
162 2
Now that the language is getting stable, and that the Idris book,    Type-driven Development with Idrisis nearing publication, it’s getting close to time to release version 1.0.  
  We’ll shortly be releasing Idris version 0.99, which is essentially an alpha release of 1.0, and we’ll keep releasing updates until 1.0 is ready, probably around February 2017. There’s still plenty to do, which we’ll be working on over the next few weeks, mostly relating to stability and efficiency, fixing as many issues as we reasonably can, and committing to various minor decisions that we’ve been putting off.
  What do we mean by “1.0”?

  Mostly, what we mean by calling a release “1.0” is that there are large parts of the language and libraries that we now consider stable, and we promise not to change them without also changing the version number appropriately. In particular, if you have a program which compiles with Idris 1.0 and its Prelude and Base libraries, you should also expect it to compile with any version 1.x. (Assuming you aren’t relying on the behaviour of a bug, at least :))
  Specifically, when we release version 1.0, the following will be stable:
  
       
  • All of the language, except those parts which require a      %languagepragma to use   
  • Everything in      prelude, except      Language.Reflection   
  • Everything in      base, except modules in the      Language.Reflectionpart of the hierarchy  
  In version 1.0, a    %languagepragma will be required to access: reflection mechanisms (that is, error reflection, elaboration reflection and reflection functions), uniqueness types and    dslnotation.  
  The other packages distributed with Idris,    contrib,    effects, and    pruviloj, may yet change. In particular,    contribremains a place for new modules to be tested, and    effectsis likely to be deprecated in favour of a    new libraryat some point.  
  Furthermore, the IDE protocol will remain backwards compatible throughout 1.0.x releases.
  Will version 1.0 be “Production Ready”?

  Idris remains primarily a research tool, with the goals of exploring the possibilities of software development with dependent types, and particularly aiming to make theorem proving and verification techniques accessible to software developers in general. We’re not an Apple or a Google or [insert large software company here] so we can’t commit to supporting the language in the long term, or make any guarantees about the quality of the implementation. There’s certainly still plenty of things we’d like to do to make it better.
  All that said, if you’re willing to get your hands dirty, or have any resources which you think can help us, please do get in touch!
shunng 发表于 2016-12-2 03:14:55
顶贴不认真,大脑有问题。
回复 支持 反对

使用道具 举报

淘旅游 发表于 2016-12-2 03:30:09
生我之前谁是我,生我之后我是谁?  
回复 支持 反对

使用道具 举报

我要投稿

推荐阅读


回页顶回复上一篇下一篇回列表
手机版/c.CoLaBug.com ( 粤ICP备05003221号 | 粤公网安备 44010402000842号 )

© 2001-2017 Comsenz Inc.

返回顶部 返回列表