Stream: Isabelle/ML

Topic: New Environment Variable

Hanna Lachnitt (Oct 21 2023 at 19:15):

Hi everyone,

I have a file MY_TOOL.thy. I am trying to add a new variable $MY_TOOL_HOME that contains the directory of MY_TOOL without hardcoding it.

I see two ways:

1. I looked up how ISABELLE_HOME is handled:

ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"

is set in build_release.scala. I have not worked with scala before and am not sure how to connect it to my current theory.

2. To have a separate settings file for my project folder such as .isabelle/etc/settings for my project and add the variable there (how do I do that dynamically?). I looked at getenv but am not completely sure how to access my new settings file.

Can anyone explain to me what the best way is and how to get to my goal?

Lukas Stevens (Oct 21 2023 at 19:40):

Where are you planning to use the variable $MY_TOOL_HOME? In independent shell scripts?

Hanna Lachnitt (Oct 21 2023 at 23:05):

In the theory itself. As an argument to a command I wrote.

Hanna Lachnitt (Oct 21 2023 at 23:07):

In ML I can write OS.FileSys.getDir() to get the current directory (the one isabelle is started in) and I am sure that there is a way to get the one of the current file. But then, when I want to use the variable that contains that directory I would need to write a keywords for it which does not seem right for a path variable like this

Lukas Stevens (Oct 21 2023 at 23:09):

You could try passing ML code that retrieves the directory to the command that you wrote. The command can then evaluate the code to get the directory.

Hanna Lachnitt (Oct 21 2023 at 23:13):

Thanks, that sounds great! How do I do that? They way I know to do something like this is to define a new keyword

keywords "my_new_command" :: diag

and then do something like this:

val _ = Outer_Syntax.local_theory \<^command_keyword>‹my_new_command› ...

Lukas Stevens (Oct 21 2023 at 23:18):

I don't know if it is the best example but @Kevin Kappelmann logger antiquotation parses ML code and evaluates it to determine log levels. looking at the ML command is easier.

Lukas Stevens (Oct 21 2023 at 23:21):

Hanna Lachnitt said:

Thanks, that sounds great! How do I do that? They way I know to do something like this is to define a new keyword

keywords "my_new_command" :: diag

and then do something like this:

val _ = Outer_Syntax.local_theory \<^command_keyword>‹my_new_command› ...

The approach is the same. You just use Parse.embeddedor Parse.ML_source to parse ML code and then other functions (not an expert there) to evaluate the code.

Lukas Stevens (Oct 21 2023 at 23:21):

Perhaps it is easier to look at the implementation of the ML command

Hanna Lachnitt (Oct 21 2023 at 23:23):

Thanks, I'll look into it! It's not super critical but it would be a nice feature for my tool

Kevin Kappelmann (Oct 23 2023 at 06:51):

Hanna Lachnitt said:

In ML I can write OS.FileSys.getDir() to get the current directory (the one isabelle is started in) and I am sure that there is a way to get the one of the current file. But then, when I want to use the variable that contains that directory I would need to write a keywords for it which does not seem right for a path variable like this

Do you really need to pass the directory as an argument to the command or is it that you always pass the same argument (i.e. the directory of your tool) to the command anyway?
In the latter case, just get rid of the argument and use ML to retrieve the directory.
In the former, you can use this to evaluate parsed ML code as an attribute, and here, at ML_int, you can see how one might use this attribute evaluation to obtain a primitive value from the parsed ML code. Beware: it is kind of a hack because it requires the invariant that the name of the ML structure that evaluates your code won't be shadowed in the future (which you cannot guarantee in general). Only use this if you know what you are doing :upside_down:

Last updated: May 04 2024 at 08:17 UTC