michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/private): use environment fingerprint to compute private decls "unique" identifier

Browse source 
fixes #648
This commit is contained in:
Leonardo de Moura 2015-06-01 22:21:31 -07:00
parent 4ace996057
commit d6997300f1
2 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/private.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "library/private.h" #include "library/private.h"
#include "library/module.h" #include "library/module.h"
#include "library/kernel_bindings.h" #include "library/kernel_bindings.h"
#include "library/fingerprint.h"
namespace lean { namespace lean {
struct private_ext : public environment_extension { struct private_ext : public environment_extension {
@ -43,6 +44,9 @@ static environment preserve_private_data(environment const & env, name const & r
pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) { pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
private_ext ext = get_extension(env); private_ext ext = get_extension(env);
unsigned h = hash(n.hash(), ext.m_counter); unsigned h = hash(n.hash(), ext.m_counter);
uint64 f = get_fingerprint(env);
h = hash(h, static_cast<unsigned>(f >> 32));
h = hash(h, static_cast<unsigned>(f));
if (extra_hash) if (extra_hash)
h = hash(h, *extra_hash); h = hash(h, *extra_hash);
name r = name(*g_private, h) + n; name r = name(*g_private, h) + n;

1
tests/lean/hott/648.hlean Normal file
View file

@ -0,0 +1 @@
import hit.colimit hit.pushout