Dynamic reloading shared library

Stream: lean4

[Tomas Skrivan]

I wrote a plugin for Houdini(software like Blender) where I'm using Lean as a scripting language. This requires building shared library out of a Lean code and dynamically reloading it whenever I change the Lean code.

For example, I have a lean file Script.leanand create libScript.so which contains some function void run() which I call from Houdini. When I changes Script.lean I need to reaload libScript.so to get a new version of void run(). I do this in couple of steps:

1. unload old libScript.so
2. unload libleanshared.so
3. load libleanshared.so
4. load new libScript.so
   This works fine.

The problem is when I want to use mathlib. To do that I need to build shared library for mathlib and all of its dependencies. So the process is

1. unload old libScript.so
2. unload libleanshared.so,libLake.so, libStd.so, libQq.so, libAesop.so, libCli.so, libProofWidgets.so, libImportGraph.so,libMathlib.so
3. load libleanshared.so,libLake.so, libStd.so, libQq.so, libAesop.so, libCli.so, libProofWidgets.so, libImportGraph.so,libMathlib.so
4. load new libScript.so

This does not work. I get a crash once I call void run() after a reload. I'm still paying around with debugger to get any kind of useful error message.

One potentially odd thing I had to do is that I had to turn libLake.a into libLake.so because when loadinglibImportGraph.so I was getting error about missing initialize_Lake_Load_Manifest and l_Lake_Manifest_load_x3f.

Is mathlib or any of its dependencies doing something that prevents such reloading?

[Tomas Skrivan]

Nevermind I was doing something stupid and accidentally I wasn't properly unloading all those libraries. Everything works now.