diff --git a/library/Makefile.common b/library/Makefile.common
index 35a87ef908..cabff59ef1 100644
--- a/library/Makefile.common
+++ b/library/Makefile.common
@@ -1,9 +1,12 @@
 TOP := $(dir $(lastword $(MAKEFILE_LIST)))
-DIR = $(shell pwd)
-LEAN_FILES = $(shell find $(DIR) -type f -name '*.lean')
-OLEAN_FILES = $(LEAN_FILES:.lean=.olean)
-DEP_FILES = $(LEAN_FILES:.lean=.d)
-LEAN_VERSION_FILE = $(shell dirname $(LEAN))/version
+DIR := $(shell pwd)
+LEAN_FILES := $(shell find $(DIR) -type f -name '*.lean')
+OLEAN_FILES := $(LEAN_FILES:.lean=.olean)
+ILEAN_FILES := $(LEAN_FILES:.lean=.ilean)
+DEP_FILES := $(LEAN_FILES:.lean=.d)
+LEAN_BIN_DIR := $(dir $(LEAN))
+LEAN_VERSION_FILE := $(LEAN_BIN_DIR)version
+LTAGS := $(LEAN_BIN_DIR)ltags
 
 all: $(OLEAN_FILES) $(DEP_FILES)
 
@@ -20,9 +23,17 @@ all: $(OLEAN_FILES) $(DEP_FILES)
 	@tr "\n" " " < $@.tmp >> $@
 	@rm -f $@.tmp
 
+%.ilean: %.lean %.olean $(LEAN_VERSION_FILE)
+	$(LEAN) $(LEAN_OPTIONS) $< -i $@
+
+etags tags: TAGS
+
+TAGS: $(ILEAN_FILES)
+	$(LTAGS)
+
 -include $(LEAN_FILES:.lean=.d)
 
-.PHONY: all clean
+.PHONY: all clean tags etags gtags
 
 clean:
 	find . -type f -name "*.olean" -delete