小编Joh*_* V.的帖子

Agda中有限集的定义

我是Agda的新手.我正在阅读Ana Bove和Peter Dybjer的论文"工作中的依赖类型".我不理解有限集的讨论(在我的副本中的第15页).

本文定义了一种Fin类型:

data Fin : Nat -> Set where
    fzero : {n : Nat} -> Fin (succ n)
    fsucc : {n : Nat} -> Fin n -> Fin (succ n)

Run Code Online (Sandbox Code Playgroud)

我一定错过了一些明显的东西.我不明白这个定义是如何工作的.有人可以简单地将定义翻译Fin成日常英语吗？这可能是我需要理解本文的这一部分.

感谢您抽出宝贵时间阅读我的问题.我很感激.

agda

Joh*_* V.

lucky-day

19
推荐指数

1
解决办法

1563
查看次数

Java Native Interface(JNI)是否受C++ ABI兼容性问题的影响？

我正在开发一个Java应用程序.我想使用Java Native Interface(JNI)来调用C++库中的函数.我可以访问C++库的代码,但我可以重建它,但我可能需要.(例如,我可以静态链接C++运行时.)

我可以要求我的用户拥有JRE 6或更高版本,但我不能要求他们拥有任何特定的C++运行时.

一位同事向我指出了这篇博客文章:http://www.trilithium.com/johan/2005/06/static-libstdc/,它建议不要使用动态加载的C++代码.

另一位同事向我指出了这个错误报告:http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=4694590,详细说明了如何在Java 1.4.2中解决这些问题.

根据我的理解,问题的要点是libstdc ++的二进制接口经常发生变化.如果C++应用程序加载了使用不同编译器构建的C++共享库,则会同时将两个不兼容的libstdc ++库加载到内存中.

错误报告解释了Java 1.4.2的解决方案:"我们静态链接JDK中的C++运行时并启用链接器脚本以隐藏libstdc ++和其他内部符号中的符号.结果,这些符号对JNI代码变得不可见,并且当某些符号时本机代码需要调用C++运行时,调用将使用适当的libstdc ++解析.所以.还有两个libstdc ++.所以同时加载,但它应该是良性的."

我有几个问题.

首先,OpenJDK是否继续采用这种方法？

[ 编辑:我在OpenJDK的build-dev邮件列表中问过这个问题.答案是肯定的,HotSpot仍然静态地链接libstdc ++,但显然"大多数Linux发行版补丁出来".另一位开发人员指出,这甚至不需要补丁:"设置STATIC_CXX = false应该足够了(默认为true)."]

其次,即使在这种情况下,拥有两个不兼容的libstdc ++是否真的是良性的.所以同时加载？

第三,这种方法(隐藏JDK中的符号)是否解决了所有兼容性问题？

上面引用的博客文章警告说"针对不同ABI编译的代码根本不是二进制兼容的".后来,"语言运行时支持通常依赖于一些共享数据,例如访问某种锁或全局数据结构(类似于C程序需要共享错误的方式)."

这使得听起来无法解决问题.

再说一次,也许ABI不兼容不再是问题.博客文章已有六年多了.另一个stackoverflow问题(GCC ABI兼容性)的答案断言"自从gcc-3.4.0起,ABI是向前兼容的".这是成功的吗？

我对这些问题的任何指导表示感谢.(嘿,谢谢阅读所有这些!)

EDITS

我的问题变得越来越长,所以我没有详细说明.解决威尔的评论: