More on Pledges

[gebner]

I now get an error when building pulse:

* Warning 285 at Pulse.Lib.Stick.fst(20,21-20,26):
  - module not found in search path: pulse.lib.trade

* Error 128 at Pulse.Lib.Stick.fst(20,21-20,26):
  - Module Pulse.Lib.Trade cannot be found

1 error was reported (see above)
make: *** [../Makefile.pulse.common:64: _output/cache/Pulse.Lib.Stick.fst.checked] Error 1

[mtzguido]

This may be a stale .depend file, could you run find . -name '*.dep*' -delete and retry?

[gebner]

That was my first instinct as well, but it didn't help. FWIW I get the error when running:

make verify -C share/steel/examples/pulse/lib/

[mtzguido]

Ah, thanks, indeed I broke that rule. This fixes it, will get it to main:

commit e167077f740b03377bc6aff09eae7f1703cd663f (HEAD -> main)
Author: Guido Martínez <mtzguido@gmail.com>
Date:   Tue Feb 6 13:01:20 2024 -0800

    pulse/lib/Makefile: fix include path

diff --git a/share/steel/examples/pulse/lib/Makefile b/share/steel/examples/pulse/lib/Makefile
index 62aa01b2..a1f8556f 100644
--- a/share/steel/examples/pulse/lib/Makefile
+++ b/share/steel/examples/pulse/lib/Makefile
@@ -1,5 +1,6 @@
 STEEL_HOME=../../../../..
 FSTAR_FILES := $(wildcard *.fst *.fsti)
+INCLUDE_PATHS=pledge
 include ../Makefile.pulse.common

 %.fst-in,%.fsti-in:

[gebner]

Is there actually a reason we don't build that target by default?

[mtzguido]

We build the parent directory (share/steel/examples/pulse) which generates a (bigger) .depend file, and checks all the files under lib/ too. This makefile is not hierarchical, it's just separate from this one, so if we were to also make this target we would build everything under lib twice. I guess this target is more of a convenience feature.. ideally it would reuse the dependency analysis of the parent but just restrict to building files under lib.