Building lean3 on macos 10.14

Stream: general

[Scott Morrison]

Has anyone successfully built lean3 on macos recently? I get an error:

/Users/scott/projects/lean/lean/src/frontends/lean/widget.cpp:436:24: error: use of overloaded operator '+=' is ambiguous (with
      operand types 'std::string' (aka 'basic_string<char, char_traits<char>, allocator<char> >') and 'json' (aka 'basic_json<>'))
                    cn += value;
                    ~~ ^  ~~~~~

in widget.cpp.

I think I'm following the vanilla build instructions...

[Scott Morrison]

I have a work-around that lets it compile, but then widgets are broken in VSCode.

[Scott Morrison]

I am using 10.14 still.

[Gabriel Ebner]

Does this work?

cn += value.get<std::string>();

[Scott Morrison]

Looks good.

https://github.com/leanprover-community/lean/pull/606